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.

<UL>

<LI> <A HREF = "holmes/omnibus.mk2">omnibus.mk2</A>: My current
universal script.

<LI> <A HREF = "holmes/structural.mk2">structural.mk2</A>: Structural
tactics.  Programming operations on tactics, including a loop
construction.  A synthetic abstraction algorithm.

<LI> <A HREF = "holmes/typestuff.mk2">typestuff.mk2</A>: Tactics for
managing type labels.  Type constructors (except for subtyping, which
needs the choice operator).

<LI> <A HREF = "holmes/lambda.mk2">lambda.mk2</A>: Tactics which allow
conversion of abstraction terms to a form with fake binding variables
and back.  Another synthetic abstraction algorithm.

<LI> <A HREF = "holmes/logicdefs.mk2">logicdefs.mk2</A>: Definitions
of first-order logic operations from the built-in logic of case
expressions.

<LI> <A HREF = "holmes/tableau.mk2">tableau.mk2</A>: Develops a
tautology checker NEWTAUT.  Proves Gries axioms for propositional
logic.

<LI> <A HREF = "holmes/logicdefs2.mk2">logicdefs2.mk2</A>
Implementation of Gries and Schneider chapter 3, by Michael Parvin --
relies on proofs of Gries axioms in tableau.mk2.

<LI> <A HREF = "holmes/logicdefs3.mk2">logicdefs3.mk2</A>
Implementation of Gries and Schneider chapter 3, by Michael Parvin --
Gries axioms are taken as axioms: depends only on structural.mk2.

<LI> <A HREF = "holmes/logic_tools.mk2">logic_tools.mk2</A>
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."

<LI> <A HREF = "holmes/tableau2.mk2">tableau2.mk2</A> Package
implementing tableau proofs, a complete technique of first-order
reasoning.  Also introduces the axiom of choice and the subtyping
constructor.

<LI><A HREF = "holmes/gries9.mk2">gries9.mk2</A>  Brief file with
definition of ranged quantifiers and a few results from Gries chapter 9.

<LI><A HREF = "holmes/new.quantifiers.mk2">new.quantifiers.mk2</A> 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).

<LI><A HREF = "holmes/simplesets.mk2">simplesets.mk2</A> A theory file
in basic set theory developed by Sol Espinosa at the University of
Idaho.

<LI> <A HREF ="holmes/naturals.mk2">naturals.mk2</A>: 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.

<LI> <A HREF = "holmes/algebra2.mk2">algebra2.mk2</A>: Some theorems
of algebra and arithmetic.  Also, some general-purpose tactics of an
abstract algebraic character.  This file requires logicdefs2.mk2.

<LI> <A HREF = "holmes/natorder.mk2">natorder.mk2</A>: Theorems about
the order properties of the natural numbers (Sol Espinosa).  This file
has been modified; see version notes of May 29, 1998.

<LI> <A HREF = "holmes/evenodd.mk2">evenodd.mk2</A>: Two theorems
about even and odd numbers; examples of extended induction proofs.
This file requires tableau2 and logic_tools.

<LI> <A HREF = "holmes/programs.mk2">programs.mk2</A>: 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.

<LI> <A HREF = "holmes/peano.mk2">peano.mk2</A>: 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.

<LI> <A HREF = "holmes/collapse.mk2">collapse.mk2</A> 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.

<LI> <A HREF = "holmes/realorder.mk2">realorder.mk2</A> 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.

<LI> <A HREF = "holmes/mwu_subtraction.mk2">mwu_subtraction.mk2</A>
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.

<LI> <A HREF = "holmes/mwu_evenodd.mk2">mwu_evenodd.mk2</A>
Some theorems on the concepts "even" and "odd"  proved by Minglong Wu;
mwu_subtraction.mk2 is required.

<LI> <A HREF = "holmes/combinators.mk2">combinators.mk2</A> 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.

<LI> <A HREF = "holmes/cylinders.mk2">cylinders.mk2</A> 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...

<LI> <A HREF = "holmes/concepts3.mk2">concepts3.mk2</A> 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.

<LI> <STRONG>Pending:</STRONG> theory files on set theory, the theory
of order on the natural numbers, another version of Gries chs. 8 and
9, and more...

</UL>

The files should be given the indicated names, since some invoke others. <P>