Admin/page/index.html
author wenzelm
Fri Jan 22 17:47:46 1999 +0100 (1999-01-22)
changeset 6150 71974ec3ebfb
parent 6149 372919b37b5d
child 6411 07e95e4cfefe
permissions -rw-r--r--
tuned;
     1 <html>
     2 
     3 <head>
     4 <!-- $Id$ -->
     5 <title>Isabelle</title>
     6 </head>
     7 
     8 <body>
     9 
    10 <h1>Isabelle </h1> <a href="http://isabelle.in.tum.de/logo/"><img
    11 src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a>
    12 
    13 <p>
    14 
    15 <strong>Isabelle</strong> is a popular generic theorem proving
    16 environment developed at Cambridge University (<a
    17 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
    18 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
    19 
    20 <p>
    21 
    22 <a
    23 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
    24 src="cambridge.gif" width=145 border=0 align=right
    25 alt="[Cambridge logo]"></a> <a
    26 href="http://isabelle.in.tum.de/munich.html"><img src="munich.gif"
    27 width=48 border=0 align=right alt="[Munich logo]"></a> This page
    28 provides general information on Isabelle, more specific information is
    29 available from the local pages
    30 
    31 <ul>
    32 
    33 <li> <a
    34 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
    35 at Cambridge</strong></a> 
    36 
    37 <li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle
    38 at Munich</strong></a>
    39 
    40 </ul>
    41 
    42 See there for information on projects done with Isabelle, mailing list
    43 archives, research papers, the Isabelle bibliography, and Isabelle
    44 workshops and courses.
    45 
    46 
    47 <h2>Obtaining Isabelle</h2>
    48 
    49 The latest version is <strong>Isabelle98-1</strong>, it is available
    50 from several <a href="dist/">mirror sites</a>.
    51 
    52 
    53 <h2>What is  Isabelle?</h2>
    54 
    55 Isabelle can be viewed from two main perspectives.  On the one hand it
    56 may serve as a generic framework for rapid prototyping of deductive
    57 systems.  On the other hand, major existing logics like
    58 <strong>Isabelle/HOL</strong> provide a theorem proving environment
    59 ready to use for sizable applications.
    60 
    61 
    62 <h3>Isabelle's Logics</h3>
    63 
    64 The Isabelle distribution includes a large body of object logics and
    65 other examples (see the <a href="library/">Isabelle theory
    66 library</a>).
    67 
    68 <dl>
    69 
    70 <dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is a
    71 version of classical higher-order logic resembling that of the <A
    72 HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL
    73 System</A>.
    74 
    75 <dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
    76 adds Scott's Logic for Computable Functions (domain theory) to HOL.
    77 
    78 <dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
    79 provides basic classical and intuitionistic first-order logic.  It is
    80 polymorphic.
    81 
    82 <dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offers
    83 a formulation of Zermelo-Fraenkel set theory on top of FOL.
    84 
    85 </dl>
    86 
    87 <p>
    88 
    89 Isabelle/HOL is currently the best developed object logic, including
    90 an extensive library of (concrete) mathematics, and various packages
    91 for advanced definitional concepts (like (co-)inductive sets and
    92 types, well-founded recursion etc.).  The distribution also includes
    93 some large applications, for example correctness proofs of
    94 cryptographic protocols (<a href="library/HOL/Auth/">HOL/Auth</a>) or
    95 communication protocols (<a href="library/HOLCF/IOA/">HOLCF/IOA</a>).
    96 
    97 <p>
    98 
    99 Isabelle/ZF provides another starting point for applications, with a
   100 slightly less developed library.  Its definitional packages are
   101 similar to those of Isabelle/HOL.  Untyped ZF provides more advanced
   102 constructions for sets than simply-typed HOL.
   103 
   104 <p>
   105 
   106 There are a few minor object logics that may serve as further
   107 examples: <a href="library/CTT/">CTT</a> is an extensional version of
   108 Martin-L&ouml;f's Type Theory, <a href="library/Cube/">Cube</a> is
   109 Barendregt's Lambda Cube.  There are also some sequent calculus
   110 examples under <a href="library/Sequents/">Sequents</a>, including
   111 modal and linear logics.  Again see the <a href="library/">Isabelle
   112 theory library</a> for other examples.
   113 
   114 
   115 <h3>Defining Logics</h3>
   116 
   117 Logics are not hard-wired into Isabelle, but formulated within
   118 Isabelle's meta logic: <strong>Isabelle/Pure</strong>.  There are
   119 quite a lot of syntactic and deductive tools available in generic
   120 Isabelle.  Thus defining new logics or extending existing ones
   121 basically works as follows:
   122 
   123 <ol>
   124 
   125 <li> declare concrete syntax (via mixfix grammar and syntax macros),
   126 
   127 <li> declare abstract syntax (as higher-order constants),
   128 
   129 <li> declare inference rules (as meta-logical propositions),
   130 
   131 <li> instantiate generic automatic proof tools (simplifier, classical
   132 tableau prover etc.),
   133 
   134 <li> manually code special proof procedures (via tacticals or
   135 hand-written ML).
   136 
   137 </ol>
   138 
   139 The first three steps above are fully declarative and involve no ML
   140 programming at all.  Thus one already gets a decent deductive
   141 environment based on primitive inferences (by employing the built-in
   142 mechanisms of Isabelle/Pure, in particular higher-order unification
   143 and resolution).
   144 
   145 For sizable applications some degree of automated reasoning is
   146 essential.  Instantiating existing tools like the classical tableau
   147 prover involves only minimal ML-based setup.  One may also write
   148 arbitrary proof procedures or even theory extension packages in ML,
   149 without breaching system soundness (Isabelle follows the well-known
   150 <em>LCF system approach</em> to achieve a secure system).
   151 
   152 
   153 <h2>Mailing list</h2>
   154 
   155 Use the mailing list <a href="mailto:
   156 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
   157 discuss problems and results.  
   158 (Why not <A HREF="mailto:lcp@@cl.cam.ac.uk">subscribe</A>?)
   159 
   160 
   161 </body>
   162 
   163 </html>