Isabelle
Isabelle is a popular generic theorem proving
environment developed at Cambridge University (Larry Paulson) and TU
Munich (Tobias Nipkow).
This page provides general information on Isabelle, more details are
available on the local Isabelle pages at Cambridge
and Munich.
See there for information on projects done with Isabelle, mailing list
archives, research papers, the Isabelle bibliography, and Isabelle
workshops and courses.
Obtaining Isabelle
The latest version is Isabelle98-1, it is available
from several mirror sites.
What is Isabelle?
Isabelle can be viewed from two main perspectives. On the one hand it
may serve as a generic framework for rapid prototyping of deductive
systems. On the other hand, major existing logics like
Isabelle/HOL provide a theorem proving environment
ready to use for sizable applications.
Isabelle's Logics
The Isabelle distribution includes a large body of object logics and
other examples (see the Isabelle theory
library).
- Isabelle/HOL
- is a
version of classical higher-order logic resembling that of the HOL
System.
- Isabelle/HOLCF
-
adds Scott's Logic for Computable Functions (domain theory) to HOL.
- Isabelle/FOL
-
provides basic classical and intuitionistic first-order logic. It is
polymorphic.
- Isabelle/ZF
- offers
a formulation of Zermelo-Fraenkel set theory on top of FOL.
Isabelle/HOL is currently the best developed object logic, including
an extensive library of (concrete) mathematics, and various packages
for advanced definitional concepts (like (co-)inductive sets and
types, well-founded recursion etc.). The distribution also includes
some large applications, for example correctness proofs of
cryptographic protocols (HOL/Auth) or
communication protocols (HOLCF/IOA).
Isabelle/ZF provides another starting point for applications, with a
slightly less developed library. Its definitional packages are
similar to those of Isabelle/HOL. Untyped ZF provides more advanced
constructions for sets than simply-typed HOL.
There are a few minor object logics that may serve as further
examples: CTT is an extensional version of
Martin-Löf's Type Theory, Cube is
Barendregt's Lambda Cube. There are also some sequent calculus
examples under Sequents, including
modal and linear logics. Again see the Isabelle
theory library for other examples.
Defining Logics
Logics are not hard-wired into Isabelle, but formulated within
Isabelle's meta logic: Isabelle/Pure. There are
quite a lot of syntactic and deductive tools available in generic
Isabelle. Thus defining new logics or extending existing ones
basically works as follows:
- declare concrete syntax (via mixfix grammar and syntax macros),
- declare abstract syntax (as higher-order constants),
- declare inference rules (as meta-logical propositions),
- instantiate generic automatic proof tools (simplifier, classical
tableau prover etc.),
- manually code special proof procedures (via tacticals or
hand-written ML).
The first three steps above are fully declarative and involve no ML
programming at all. Thus one already gets a decent deductive
environment based on primitive inferences (by employing the built-in
mechanisms of Isabelle/Pure, in particular higher-order unification
and resolution).
For sizable applications some degree of automated reasoning is
essential. Instantiating existing tools like the classical tableau
prover involves only minimal ML-based setup. One may also write
arbitrary proof procedures or even theory extension packages in ML,
without breaching system soundness (Isabelle follows the well-known
LCF system approach to achieve a secure system).
Mailing list
Use the mailing list isabelle-users@cl.cam.ac.uk to
discuss problems and results.
(Why not subscribe?)