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

author | paulson |

Wed, 09 Oct 1996 13:39:25 +0200 | |

changeset 2077 | 477e80fe0e9b |

parent 2076 | ec8857a115af |

child 2078 | b198b3d46fb4 |

Plain text README files now redundant due to HTML versions

src/Cube/README | file | annotate | diff | comparison | revisions | |

src/FOL/README | file | annotate | diff | comparison | revisions | |

src/HOL/README | file | annotate | diff | comparison | revisions | |

src/HOLCF/README | file | annotate | diff | comparison | revisions | |

src/LCF/README | file | annotate | diff | comparison | revisions | |

src/LK/README | file | annotate | diff | comparison | revisions | |

src/Modal/README | file | annotate | diff | comparison | revisions | |

src/ZF/README | file | annotate | diff | comparison | revisions |

--- a/src/Cube/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ - Cube: Barendregt's Lambda-Cube - -This directory contains the Standard ML sources of the Isabelle system for -the Lambda-Cube. Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML"; - -Makefile -- compiles the files under Poly/ML or SML of New Jersey - -ex.ML -- examples file. To execute them, enter an ML image -containing Cube and type: use "ex.ML"; - -NB: the formalization is not completely sound! It does not enforce -distinctness of variable names in contexts! - -For more information about the Lambda-Cube, see - H. Barendregt - Introduction to Generalised Type Systems - J. Functional Programming -

--- a/src/FOL/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ - FOL: First-Order Logic with Natural Deduction - -This directory contains the Standard ML sources of the Isabelle system for -First-Order Logic (constructive and classical versions). For a classical -sequent calculus, see LK. Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML"; - -Makefile -- compiles the files under Poly/ML or SML of New Jersey - -ex -- subdirectory containing examples. To execute them, enter an ML image -containing FOL and type: use "ex/ROOT.ML"; - -Useful references on First-Order Logic: - - Antony Galton, Logic for Information Technology (Wiley, 1990) - - Michael Dummett, Elements of Intuitionism (Oxford, 1977) \ No newline at end of file

--- a/src/HOL/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ - HOL: Higher-Order Logic with curried functions - -This directory contains the Standard ML sources of the Isabelle system for -Higher-Order Logic with curried functions. Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML"; - -Makefile -- compiles the files under Poly/ML or SML of New Jersey - -ex -- subdirectory containing examples. To execute them, enter an ML image -containing HOL and type: use "ex/ROOT.ML"; - -Subst -- subdirectory defining a theory of substitution and unification. - -Useful references on Higher-Order Logic: - - P. B. Andrews, - An Introduction to Mathematical Logic and Type Theory - (Academic Press, 1986). - - J. Lambek and P. J. Scott, - Introduction to Higher Order Categorical Logic (CUP, 1986)

--- a/src/HOLCF/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -HOLCF: A higher order version of LCF based on Isabelle HOL -========================================================== - -Author: Franz Regensburger -Copyright 1995 Technische Universitaet Muenchen - -Version: 2.0 -Date: 16.08.95 - -A detailed description of the entire development can be found in - -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF, - Dissertation, Technische Universit"at M"unchen, 1994 - -Changes: -14.10.94 New translation mechanism for continuous infixes -18.05.95 Conversion to curried version of HOL. - -28.06.95 The old uncurried version of HOLCF is no longer supported - in the distribution. - -18.08.95 added sections axioms, ops, domain, generated - and optional 8bit support -

--- a/src/LCF/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ - LCF: Logic for Computable Functions - -This directory contains the Standard ML sources of the Isabelle system for -LCF. It is loaded upon FOL, not Pure Isabelle. Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing FOL and -type: use "ROOT.ML"; - -Makefile -- compiles the files under Poly/ML or SML of New Jersey - -ex.ML -- files containing examples. To execute them, enter an ML image -containing LCF and type: use "ex.ML"; - -Useful references on LCF: - - Lawrence C. Paulson, - Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) -

--- a/src/LK/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ - LK: Classical First-Order Sequent Calculus - -This directory contains the Standard ML sources of the Isabelle system for -First-Order Logic as a classical sequent calculus. (For a Natural Deduction -version, see FOL.) Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML"; - -Makefile -- compiles the files under Poly/ML or SML of New Jersey - -ex -- subdirectory containing examples. To execute them, enter an ML image -containing LK and type: use "ex/ROOT.ML"; - - -Useful references on sequent calculi: - - Jean Gallier, Logic for Computer Science (Harper&Row, 1986) - - G. Takeuti, Proof Theory (North Holland, 1987)

--- a/src/Modal/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ - Modal: First-Order Modal Sequent Calculus - -This directory contains the Standard ML sources of the Isabelle system for -Modal Logic. Important files include - -ROOT.ML -- loads all source files. Enter an ML image containing LK - and type: use "ROOT.ML"; - -ex -- subdirectory containing examples. Files, Tthms.ML, S4thms.ML and -S43thms.ML contain the theorems of Modal Logics, so arranged since -T<S4<S43. To execute them, enter an ML image containing Modal and type - use "ex/ROOT.ML"; - -Thanks to Rajeev Gore' for supplying the inference system for S43. - -Useful references on Modal Logics: - - Melvin C Fitting, - Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983) - - Lincoln A. Wallen, - Automated Deduction in Nonclassical Logics (MIT Press, 1990)

--- a/src/ZF/README Wed Oct 09 13:38:11 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,71 +0,0 @@ - ZF: Zermelo-Fraenkel Set Theory - -This directory contains the Standard ML sources of the Isabelle system for -ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files -include - -Makefile -- compiles the files under Poly/ML or SML of New Jersey. Can also -run all the tests described below. - -ROOT.ML -- loads all source files. Enter an ML image containing FOL and -type: use "ROOT.ML"; - -There are also several subdirectories of examples. To execute the examples on -some directory <Dir>, enter an ML image containing ZF and type - use "<Dir>/ROOT.ML"; - -AC -- subdirectory containing proofs from the book "Equivalents of the Axiom -of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof -Gr`abczewski. - -Coind -- subdirectory containing a large example of proof by co-induction. It -is by Jacob Frost following a paper by Robin Milner and Mads Tofte. - -IMP -- subdirectory containing a semantics equivalence proof between -operational and denotational definitions of a simple programming language. -Thanks to Heiko Loetzbeyer & Robert Sandner. - -Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is -by Ole Rasmussen, following the Coq proof by Gérard Huet. - -ex -- subdirectory containing various examples. - -Isabelle/ZF formalizes the greater part of elementary set theory, including -relations, functions, injections, surjections, ordinals and cardinals. -Results proved include Cantor's Theorem, the Recursion Theorem, the -Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem. - -Isabelle/ZF also provides theories of lists, trees, etc., for formalizing -computational notions. It supports inductive definitions of -infinite-branching trees for any cardinality of branching. - -Useful references for Isabelle/ZF: - - Lawrence C. Paulson, - Set theory for verification: I. From foundations to functions. - J. Automated Reasoning 11 (1993), 353-389. - - Lawrence C. Paulson, - Set theory for verification: II. Induction and recursion. - Report 312, Computer Lab (1993). - - Lawrence C. Paulson, - A fixedpoint approach to implementing (co)inductive definitions. - In: A. Bundy (editor), - CADE-12: 12th International Conference on Automated Deduction, - (Springer LNAI 814, 1994), 148-161. - -Useful references on ZF set theory: - - Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) - - Patrick Suppes, Axiomatic Set Theory (Dover, 1972) - - Keith J. Devlin, - Fundamentals of Contemporary Set Theory (Springer, 1979) - - Kenneth Kunen - Set Theory: An Introduction to Independence Proofs - (North-Holland, 1980) - -$Id$