CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

Isabelle: Automated generic theorem prover

areas/reasonng/atp/systems/isabelle/
Isabelle is a highly automated generic theorem prover written in Standard ML. New logics are introduced by specifying their syntax and rules of inference. Proof procedures can be expressed using tactics and tacticals. Isabelle comes with 8 different logics, including LCF, some modal logics, first-order logic, Zermelo-Fraenkel set theory, and higher-order logic. Isabelle-93 is not upwardly compatible with its predecessor, but comes with advice on converting to the new simplifier. The Elle Verification Environment for ML (requires Isabelle-92), the archives of the isabelle-users mailing list, and Martin Coen's Substitutions system are included. 
Origin:   

   ftp.cl.cam.ac.uk:/ml/ [128.232.0.56] (Univ. of Cambridge)
   ftp.informatik.tu-muenchen.de:/lehrstuhl/nipkow/ [131.159.0.198]
   (University of Munich)
   as the file Isabelle93.tar.gz
   ftp.dcs.ed.ac.uk:/pub/da/
   as the file isa-mode.tar.gz (Emacs-Lisp package for Isabelle)
Version: Isabelle 93 (16-DEC-93); Elle 2.4 (6-MAY-94) Requires: Standard ML Updated: Thu Sep 8 19:00:06 1994 CD-ROM: Prime Time Freeware for AI, Issue 1-1 Mailing List: isabelle-users@cl.cam.ac.uk (moderated) Author(s): Lawrence C Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England Tel: +44-223-334600 Fax: +44-223-334678 [Isabelle] Tobias Nipkow Institut f\"ur Informatik TU M\"unchen 80290 M\"unchen Germany Tel: +49-89-21052690 Fax: +49-89-21058183 [Isabelle] David Aspinall Department of Computer Science University of Edinburgh King's Buildings Edinburgh Tel: +44 31 650 5898 [Emacs-Lisp package for Isabelle] Keywords: Authors!Aspinall, Authors!Coen, Authors!Nipkow, Authors!Paulson, Automated Reasoning, Denotational Semantics, First Order Logic, Higher Order Logic, Inference, Isabelle, LCF, Lazy Evaluation, ML!Code, Modal Logic, Natural Deduction, Reasoning!Automated Reasoning, Simplifiers, Theorem Proving, Univ. of Cambridge, Univ. of Munich, Zermelo-Fraenkel Set Theory References: The distribution includes extensive documentation, including a 71-page introduction, an 85-page reference manual, and a 166-page description of the various logics supplied with Isabelle.
Last Web update on Mon Feb 13 10:27:32 1995
AI.Repository@cs.cmu.edu