diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/index.html --- a/Admin/page/index.html Wed Dec 08 13:53:29 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,164 +0,0 @@ - - - - -Isabelle - - - - -

Isabelle

[Isabelle logo] - -

- -Isabelle is a popular generic theorem proving -environment developed at Cambridge University (Larry Paulson) and TU -Munich (Tobias Nipkow). - -

- - [Munich logo] This page -provides general information on Isabelle, more specific information is -available from the local pages - -

- -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 current version is Isabelle99. Several mirror -sites provide the Isabelle distribution, which -includes sources, documentation, and binary packages. - - -

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: - -
    - -
  1. declare concrete syntax (via mixfix grammar and syntax macros), - -
  2. declare abstract syntax (as higher-order constants), - -
  3. declare inference rules (as meta-logical propositions), - -
  4. instantiate generic automatic proof tools (simplifier, classical -tableau prover etc.), - -
  5. 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?) - - - - -