CTT/ReadMe

# HG changeset patch # User clasohm # Date 816610970 -3600 # Node ID 69fec018854c59c862c34e08a6f9d1e9123118dc # Parent 71b0a5d8334777bd0cc14dc9ed87ccab4b66f67d HTML version of README diff -r 71b0a5d83347 -r 69fec018854c src/CTT/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CTT/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,32 @@ +CTT/ReadMe + +

CTT: Constructive Type Theory

+ +This directory contains the Standard ML sources of the Isabelle system for +Constructive Type Theory (extensional equality, no universes). 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 CTT and type: use "ex/ROOT.ML";
+

+ +Useful references on Constructive Type Theory: + +

B. Nordström, K. Petersson and J. M. Smith,
+ Programming in Martin-Löf's Type Theory
+ (Oxford University Press, 1990) + +
Simon Thompson,
+ Type Theory and Functional Programming (Addison-Wesley, 1991) +

+ diff -r 71b0a5d83347 -r 69fec018854c src/Cube/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Cube/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,31 @@ +Cube/ReadMe + +

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

+ diff -r 71b0a5d83347 -r 69fec018854c src/HOL/README.html --- a/src/HOL/README.html Fri Nov 17 13:15:19 1995 +0100 +++ b/src/HOL/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -24,11 +24,12 @@ Useful references on Higher-Order Logic:

P. B. Andrews, An Introduction to Mathematical Logic and Type Theory -(Academic Press, 1986). +
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) +
J. Lambek and P. J. Scott,
+ Introduction to Higher Order Categorical Logic (CUP, 1986)

diff -r 71b0a5d83347 -r 69fec018854c src/HOLCF/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,36 @@ +HOLCF/ReadMe + +

HOLCF: A higher order version of LCF based on Isabelle HOL

+ +Author: Franz Regensburger
+Copyright 1995 Technische Universität München

+ +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ät München, 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, genertated + and 8bit support +

+ diff -r 71b0a5d83347 -r 69fec018854c src/LCF/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,27 @@ +LCF/ReadMe + +

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 +Isabelle and type: use "ROOT.ML";
+ +
Makefile +: compiles the files under Poly/ML or SML of New Jersey
+ +
ex.ML +: file containing examples. To execute it, enter an ML image +containing LCF and type: use "ex.ML"; +

+ +Useful references on First-Order Logic: + +

Lawrence C. Paulson,
+ Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) +

+ diff -r 71b0a5d83347 -r 69fec018854c src/LK/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LK/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,30 @@ +LK/ReadMe + +

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 First-Order Logic: + +

Jean Gallier,
+ Logic for Computer Science (Harper&Row, 1986) +
G. Takeuti,
+ Proof Theory (North Holland, 1987) +

+ diff -r 71b0a5d83347 -r 69fec018854c src/Modal/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Modal/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,30 @@ +Modal/ReadMe + +

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

+ diff -r 71b0a5d83347 -r 69fec018854c src/ZF/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,89 @@ +ZF/ReadMe + +

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

+ +