# HG changeset patch # User kleing # Date 963405988 -7200 # Node ID 21bfc8c14c3db022c18e8f808b36ce14c96de1d0 # Parent 85a5355faa9129a7b172f319345b87bf2a1a1b85 about -> logics, better access to online libraries diff -r 85a5355faa91 -r 21bfc8c14c3d Admin/page/main-content/about.content --- a/Admin/page/main-content/about.content Mon Jul 10 12:17:34 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -%title% -About Isabelle - -%body% -

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). diff -r 85a5355faa91 -r 21bfc8c14c3d Admin/page/main-content/index.content --- a/Admin/page/main-content/index.content Mon Jul 10 12:17:34 2000 +0200 +++ b/Admin/page/main-content/index.content Wed Jul 12 14:46:28 2000 +0200 @@ -13,7 +13,7 @@

-These pages provide general information on Isabelle, more specific +These pages provide general information on Isabelle, more specific information is available from the local pages

{ISABELLE}

+ +You can also browse the main Isabelle logics +HOL, HOLCF, +FOL and ZF online. + +

User interface

What is Isabelle?

Isabelle/HOL

Isabelle's Logics

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

Isabelle/Pure

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). + +

LCF system approach