Automated Reasoning

This is material related to MAT 504, Topics in Logic, for the Spring term of 1997 (MW 1:30-3:00, Fine 214), on automated reasoning. These are not full lecture notes for the course, and sometimes there is only a list of topics presented at the blackboard or computer terminal.

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

Blurb

After the media hype about the computer solution of the Robbins problem is discounted, what remains? This question can be answered only by looking into what was done.

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.

Disclaimer

Although I have worked on a proof-checking program, which I hope to have in shape to publish this year, I am not a member of the AR (automated reasoning) community and have no expertise in the field. There may well be some boners here and if so I hope that more knowledgeable people will set me (nelson@math.princeton.edu) straight. The same remarks apply to expressions of opinion, and if I slight or ignore anyone's work this is due to ignorance and not malice.

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?

Lecture 1

Like most mathematicians, I first heard of the solution of the Robbins problem from the New York Times article. Here are some corrections by William McCune, the person who solved the Robbins problem. Other comments on the article can be made...

Boolean algebra

George Boole...

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's axioms

Edward V. Huntington, Sets of independent postulates for the algebra of logic, Trans. Am. Math. Soc., vol. 5 (1904), 288-390 and (our beginning point) New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Pricipia Mathematica, ibid., vol. 35 (1933) 274-304, with a major correction in Boolean algebra. A correction., ibid., vol. 35 (1933), 557-558.

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)' = a
together with idempotency a+a = a. Huntington shows that these axioms are indeed axioms for Boolean algebra and states falsely that they are irredundant ("independent"). He gives an incorrect model purporting to satisfy the other axioms but not idempotency. In the correction he proves idempotency from the other axioms. This evidently caused him much trouble, for he thanks Mr. B. Notcutt for an essential step in the proof. I submitted the problem to McCune's automated deduction system Otter, and it proved idempotency from the other axioms in 53 seconds on tea (SUN-3/50M-4). The proof was sent to the ILF (Integration of Logical Functions) mail server in Berlin, and a few minutes later I got back an automatically generated humanly readable proof. (To be honest, I had a little trouble at first but an e-mail request for help produced an abundance of help and suggestions from Ingo Dahn of the Humboldt University -- many thanks!) Well, the output is humanly readable but the relevant substitutions to make are not always easy to see -- but the same holds for Huntington's paper.

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.

The Robbins Axioms

Herbert Robbins proposed replacing Huntington's axiom by 
(Robbins' axiom R) ((x+y)'+(x+y')')' = x
The Robbins problem is whether AC (associativity and commutativity of union) together with Robbins' axiom are an axiomatization of Boolean algebras. This is the problem that McCune solved in October 1996. Note that Robbins' axiom obviously holds in Boolean algebras.

Lecture 2

Winker's Lemma states that associativity, commutativity, Robbins' axiom, and the existence of c and d satisfying 
(Winker's condition) c+d = c
imply 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...

Demonstration 3

Hyperlinks in brackets below are local files, requiring a Mathematics Department account (but all these files are freely available from the sources indicated ). With a Mathematics Department account and on a SUN4 or SGI Irix5.3, you can use the programs (They are in /usr/local/bin, thanks to Richard Wong.)

Otter

Otter is "Organized Techniques for Theorem proving and Efficient Research", and there is a Reference Manual and Guide.

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

Using Otter...

EQP

EQP is "EQuational theorem Prover". This is the program that was used to solve the Robbins problem. There is no documentation as yet, but it is very similar to Otter. There are many example input files at this link, and here are the [source codes].

MACE

MACE (the spice, not the weapon) is "Models And Counter-Examples". The program mace is actually a tiny shell script linking otter to anldp ("Argonne National Laboratory -- Davis-Putnam"). More on the Davis-Putnam algorithm later.

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

ILF

ILF is "Integration of Logical Formulas". Send a suitably formatted proof to 
ilf-serv@mathematik.hu-berlin.de
and 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.out
The % in Otter is a comment (for the rest of the line). In idempotency.in the Otter comments %NAME: associativity, etc., are read by ILF. It is essential to put NAME: goal before the theorem being proved (all Otter proofs are by contradiction). Be sure to use lower case for names! In the TEXOP section of the document sent to the ILF mailserver, instructions for typesetting these names and various symbols are given. Also, after proof_title put the desired title between the double quotes. Between FILE .in and END_FILE put the Otter in file, and between FILE .opf and END_FILE put the Otter out file. The Otter in file must contain set(build_proof_object). Note that all Otter commands end with a period.

Lecture 4

The best reference for logic is: 
[Sh] Joseph R. Shoenfield, Mathematical Logic, Addison-Wesley,1967.
For logic oriented towards AR, see: 
[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.

First order predicate calculus with equality

Following [Sh], symbols are variables, function symbols, predicate symbols and logical operators. We take \exists, \forall, ~, |, and & as the logical operators.

Constants and predicate letters...

Index (arity) of a symbol...

Terms and formulas...

Propositional calculus

Consider only formulas made from predicate letters and the logical connectives.

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].

Lecture 5

Digression on Cook's Theorem (the NP-completeness of satisfiability for finite sets of clauses) following the exposition in 
Michael R. Garey and David S. Johnson, Computers and Intractability:
A Guide to the Theory of NP-Completeness, Freeman, 1979.

Lecture 6