Here is the relevant directory index, and this is my home page.

In my opinion, it is a significant achievement. I am skeptical about the role that automated reasoning can play in mathematics in the next few centuries, but there are interesting and non-trivial results. They lead us into an odd mixture of computer science, logic, universal algebra, pragmatic experimentation, and (so help me) elliptic curves.

The goals of this course are to describe the methodology of the field, to have fun playing with the programs Otter, Mace, and EQP that led to the solution of the Robbins problem, to look at some other programs that have been developed, to explore some of the corners of mathematics in which automatic reasoning has proved useful, to help anyone seriously wishing to apply these tools to problems of interest, and to try to estimate the promises and limitations of automatic reasoning.

The field is approached here from the consumer's perspective: What is now available that is useful to mathematicians? What can we hope for in the future? What need we fear in the future, and when if ever will a mathematical Luddite movement be born? What are the interesting conceptual and technical aspects of the field?

*The Laws of Thought*, 1854...

The usual axioms for Boolean algebra, in terms of 0, 1, union, intersection, and complement, are highly redundant...

A. N. Whitehead, *Universal Algebra*, Cambridge University
Press, 1898...

Huntington and many others use + (infix) for \cup (union) in Boolean
algebra. This is a bad notation (+ should be reserved for
symmetric difference, when regarding a Boolean algebra as a commutative
algebra -- in the usual mathematical sense -- with unit over the field
of two elements), but it has the advantage of being on the typewriter
keyboard. He uses `'` (postfix) for complement.
In his 1933 paper (p. 280 "the fourth set"),
Huntington gives the following axioms for Boolean algebra:

(Commutativity) a+b = b+a (Associativity) (a+b)+c = a+(b+c) (Huntington's axiom H) (a'+b')'+(a'+b)' = atogether with idempotency

The proof of idempotency yields as byproducts involution
`x''=x`, the uniqueness of the unit `x+x'=y+y'`
(so we can introduce a constant by `1 = x+x'` with
`0 = 1'`, and the facts that `1+x = 1` and
`0+x = x`. In complete detail... (proof at the blackboard
based on the first part of the ILF output and Huntington's
correction).
To complete the proof that Huntington's axioms characterize
Boolean algebras, we need only establish distributivity. The
other axioms (see, for example, Garrett Birkhoff and Saunders MacLane,
*A Survey of Modern Algebra, Chap. 11,* MacMillan, 1953) follow
trivially. Otter and ILF produced a
proof of distributivity.

(Robbins' axiom R) ((x+y)'+(x+y')')' = xThe

(Winker's condition) c+d = cimply Huntington's axiom and so characterize Boolean algebras. More on this later.

The proof, from McCune's preprint, that Robbins' axiom (with AC) implies the Winker condition...

- otter
- eqp
- anldp
- mace

The [source codes] consist of C scripts and a Makefile. Many [examples] are available. It is best to begin with [auto] examples.

Using Otter...

There is documentation, and here are the [source codes].

ilf-serv@mathematik.hu-berlin.deand receive back a LaTeX file of a humanly readable proof. See the ILF Server Manual for Otter proofs.

Here is an
example. After `FILE .in` comes
the file `idempotency.in` and after `FILE .opf`
comes the file `idempotency.out`, produced from the former
by the command

otter <idempotency.in >idempotency.outThe

[Sh] Joseph R. Shoenfield,For logic oriented towards AR, see:Mathematical Logic, Addison-Wesley,1967.

[ChLe] Chin-Liang Chang and Richard Char-Tung Lee,Symbolic Logic and Mechanical Theorem Proving, Academic Press,1973. [Lo] Donald W. Loveland,Automated Theorem Proving: A Logical Basis, North-Holland, 1978.

Constants and predicate letters...

Index (arity) of a symbol...

Terms and formulas...

Semantics of the propostional calculus, truth valuations (interpretations)...

Literals, clauses, conjunctive normal form, satisfiability of a set of clauses...

Davis-Putnam... [ChLe, p. 63; Lo, p. 53]

Ground resolution... [ChLe, p. 71; Lo, p. 56]

The predicate letters, or truth values, `T` and `F`.
An empty clause is `F` and an empty set (conjunction) of
clauses is `T`...

The ground resolvent operator and the ground resolution logic gR. Soundness and satisfiability-incompleteness of gR...

**Refutation Completeness Theorem**. Let S be a set
of clauses of the propositional calculus. Then S is unsatisfiable
if and only if there is a gR deduction of `F`.

First let S be finite, and consider the binary tree of all partial truth valuations. Failure node, inference node... Resolve at inference nodes...

For S infinite, use König's Lemma...

[Lo, pp. 56-72].

Michael R. Garey and David S. Johnson,Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.