General overhaul completed August 19th (except for expected student contributions -- also, results in the theory of order are not yet included.) Further changes Mar 3, 1998 (new.quantifiers became main logic script) Further changes (peano.mk2 posted) Mar 10., 1998. Further changes (natorder.mk2 posted) May 19, 1998.
• omnibus.mk2: My current universal script.
• structural.mk2: Structural tactics. Programming operations on tactics, including a loop construction. A synthetic abstraction algorithm.
• typestuff.mk2: Tactics for managing type labels. Type constructors (except for subtyping, which needs the choice operator).
• lambda.mk2: Tactics which allow conversion of abstraction terms to a form with fake binding variables and back. Another synthetic abstraction algorithm.
• logicdefs.mk2: Definitions of first-order logic operations from the built-in logic of case expressions.
• tableau.mk2: Develops a tautology checker NEWTAUT. Proves Gries axioms for propositional logic.
• logicdefs2.mk2 Implementation of Gries and Schneider chapter 3, by Michael Parvin -- relies on proofs of Gries axioms in tableau.mk2.
• logicdefs3.mk2 Implementation of Gries and Schneider chapter 3, by Michael Parvin -- Gries axioms are taken as axioms: depends only on structural.mk2.
• logic_tools.mk2 More logical results: Parvin's tactics for conversion between different forms of "implication" theorems, Alves-Foss theorems on case expressions, basic theorems about quantifiers of Holmes and Alves-Foss proved "by hand."
• tableau2.mk2 Package implementing tableau proofs, a complete technique of first-order reasoning. Also introduces the axiom of choice and the subtyping constructor.
• gries9.mk2 Brief file with definition of ranged quantifiers and a few results from Gries chapter 9.
• new.quantifiers.mk2 The new total logic script; calls gries9 (which calls earlier files) then proves new theorems from chapters 8 and 9 of Gries (the new theorems are due to Michael Parvin).
• simplesets.mk2 A theory file in basic set theory developed by Sol Espinosa at the University of Idaho.
• naturals.mk2: Beginnings of a theory of natural and real numbers, interfaced with the built-in arithmetic of the prover. Naturals are implemented as a subtype of reals; Peano axioms and elementary algebra of reals are provided and some simple theorems are proved. Order definition "LESS1" is given at the end of this file; no order theorems are proved.
• algebra2.mk2: Some theorems of algebra and arithmetic. Also, some general-purpose tactics of an abstract algebraic character. This file requires logicdefs2.mk2.
• natorder.mk2: Theorems about the order properties of the natural numbers (Sol Espinosa). This file has been modified; see version notes of May 29, 1998.
• evenodd.mk2: Two theorems about even and odd numbers; examples of extended induction proofs. This file requires tableau2 and logic_tools.
• programs.mk2: The beginnings of a development of the theory of programs in a language similar to that used in Cohen's Programming in the 90's.
• peano.mk2: A development of Peano arithmetic under Mark2, in progress. Depends on the logic file new.quantifiers.mk2, but independent of the more ad hoc development of arithmetic in naturals.mk2. Intended to illustrate proof by induction.
• collapse.mk2 A file by Michael Parvin which contains an alternate tautology checker TAUTNEW and a tactic for converting case expressions back into propositional logic. Not yet linked with other scripts; it does run correctly if run in the omnibus theory.
• realorder.mk2 A file on the theory of order on the reals (not the theory of order on the naturals being developed by others), developed from the notion of "positive real number". Still under construction; it is now invoked at the end of algebra2.mk2 in the construction of the omnibus theory.
• mwu_subtraction.mk2 Some theorems on natural number subtraction proved by Sol Espinosa and Minglong Wu; natorder.mk2 is required. Some of this was run under the new version of the prover (you can see this from the way some theorems are displayed), but the file as it stands requires the old version.
• mwu_evenodd.mk2 Some theorems on the concepts "even" and "odd" proved by Minglong Wu; mwu_subtraction.mk2 is required.
• combinators.mk2 A file under construction on the untyped combinatory logic of Curry (Jonathan Seldin take note). Abstraction and reduction algorithms in place. Strong reduction is planned. This file contains examples as well as proofs of theorems and tactics; it is a good idea to step through it manually.
• cylinders.mk2 An implementation of Tarski's "cylindrical algebra". This is a file I'm using in pure math research. It might be interesting to students as showing a different approach to boolean algebra. It would be much better if it were integrated with the structural tactics, but I was lazy...
• concepts3.mk2 A proposed implementation (I'm in the process of verifying it) of Quine's calculus of concepts, an old proposal for doing first-order logic without bound variables. The reason I'm working on it is that Quine never equipped it with axioms or rules of inference. Pure math research, probably no CS interest.
• Pending: theory files on set theory, the theory of order on the natural numbers, another version of Gries chs. 8 and 9, and more...
The files should be given the indicated names, since some invoke others.