summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 02 Nov 1998 21:15:55 +0100 | |

changeset 5790 | 57e3c7775ead |

parent 5789 | 7d4ac02677a6 |

child 5791 | 96ab3e097732 |

main Isabelle page;

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/page/index.html Mon Nov 02 21:15:55 1998 +0100 @@ -0,0 +1,139 @@ + +<html> + +<head> +<title>Isabelle</title> + +<body> + +<h1>Isabelle </h1> <a href="http://www.in.tum.de/~isabelle/logo/"><img +src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a> + +<p> + +<strong>Isabelle</strong> is a popular generic theorem proving +environment developed at Cambridge University (<a +href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU +Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). +The latest version is <strong>Isabelle98-1</strong>. It is available +from several <a href="dist/">mirror sites</a>. + +<p> + +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 object logics, like +<strong>Isabelle/HOL</strong>, provide a theorem proving environment +ready to use for sizable applications. + + +<h2>Object logics</h2> + +The Isabelle distribution includes o large body of object logics and +other examples (see the <a +href="http://www.in.tum.de/~isabelle/library/">Isabelle theory +library</a>. + +<dl> + +<dt><a +href="http://www.in.tum.de/~isabelle/library/HOL/"><strong>Isabelle/HOL</strong></a><dd> +is a version of classical higher-order logic, similar to Gordon's HOL +(it is related to Church's Simple Theory of Types). + +<dt><a +href="http://www.in.tum.de/~isabelle/library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd> +adds a considerably amount of Scott's domain theory to HOL. + +<dt><a +href="http://www.in.tum.de/~isabelle/library/FOL/"><strong>Isabelle/FOL</strong></a><dd> +provides basic classical and intuitionistic first-order (polymorphic) +logic. + +<dt><a +href="http://www.in.tum.de/~isabelle/library/ZF/"><strong>Isabelle/ZF</strong></a><dd> +offers a formulation of Zermelo-Fraenkel set theory on top of FOL. + +</dl> + +<p> + +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 (<a +href="http://www.in.tum.de/~isabelle/library/HOL/Auth/">HOL/Auth</a>). + +<p> + +Isabelle/ZF provides another starting point for applications, with a +slightly less developed library, though. Its definitional packages +are similar to those of Isabelle/HOL. Untyped ZF provides more +advanced constructions for sets than simply typed HOL. + +<p> + +There are also a few minor object logics that may serve as further +examples: <a +href="http://www.in.tum.de/~isabelle/library/CTT/">CTT</a> is an +extensional version of Martin-Löf's Type Theory, <a +href="http://www.in.tum.de/~isabelle/library/Cube/">Cube</a> is +Barendregt's Lambda Cube. There are also some sequent calculus +examples under <a +href="http://www.in.tum.de/~isabelle/library/Sequents/">Sequents</a>, +including modal or linear logics. There are a few more examples, +again see the <a +href="http://www.in.tum.de/~isabelle/library/">Isabelle theory +library</a>. + + +<h2>Defining Logics</h2> + +Logics are not hard-wired into Isabelle, but formulated within +Isabelle's meta logic: <strong>Isabelle/Pure</strong>. There are +quite a lot of syntactic and deductive tools available. Thus defining +new logics or extending existing ones basically works as follows: + +<ol> + +<li> declare concrete syntax (via mixfix grammar and syntax macros), + +<li> declare abstract syntax (as higher-order constants), + +<li> declare inference rules (as meta-logical propositions), + +<li> instantiate generic proof tools (simplifier, classical tableau +prover etc.), + +<li> manually code special proof procedures (via tacticals or hand +written ML). + +</ol> + +The first 3 steps 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"). + + +<h2>Further information</h2> + +<a href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"><img +src="cambridge.gif" width=144 align=right alt="[Cambridge]"></a> <a +href="http://www.in.tum.de/~isabelle/"><img src="munich.gif" width=47 +align=right alt="[Munich]"></a> The local Isabelle pages at <a +href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html">Cambridge</a> +and <a href="http://www.in.tum.de/~isabelle/">Munich</a> provide +further information on Isabelle and related projects. + + +</html>