Thesis

Meanwhile, and independently, Ross Overbeek was completing his dissertation at Penn State under the direction of Gene Singletary. Part of that work involved the implementation of a high-performance theorem prover, and a proof of the commutator problem was his goal. An interesting feature of this prover[20] was that although complete for first-order logic, it did not use functions. It was called FTP (for Functionless Theorem Prover), and introduced a number of features for the first time that have remained important components of the Argonne family of theorem-proving systems. It had the first efficient implementation of hyperresolution, FPA indexing, forward and backward subsumption, and weighting. It used the following algorithm for its basic loop, which remained exactly the same through several generations of systems to come.

We assume here that we start with a set of clauses divided into two sets, which we call the ``axioms'' and the ``set of support''. The following is what we refer to throughout this paper as the closure algorithm.

  2#2

This algorithm, which at the time was thought of as just one implementation of the set of support strategy, owes its long life to its (perhaps unforeseen) great adaptability. Nearly all the additions, modifications, and refinements of the next twenty years have fit into the framework of this simple algorithm. Even the parallel algorithms described in Section can be seen as small variations on this theme.

The closure algorithm computes the closure of a set of clauses under the operation of a set of inference rules, keeping an eye out for the empty clause. It is different from various other theorem-proving algorithms in two important ways.

• It differs from the ``natural deduction'' or ``agenda'' approaches in that at each step it generates all consequences of the given clause.
• It differs from the ``Prolog technology'' family of approaches in that (processed) new clauses are stored in an ever-growing database. It is considered that a lot of work went into computing them, and this work should not have to be repeated. The algorithm stops after each step to decide what to work on next.

There are many places for user control and the operation of heuristics: in the choice of the initial set of support, the choice of inference rules, the choice of given clause at the beginning of each iteration, and the choice of what to keep during post-processing.

The algorithm has thus been able to be used in a wide variety of contexts: showing that a set of clauses is unsatisfiable, executing the Knuth-Bendix completion procedure, computing the sizes of certain algebraic structures[12], designing circuits, and searching for fixed-point combinators[19]. What this says is that many problems can be usefully expressed in terms of computing (part of) the logical closure of a set of clauses.

FTP could do the commutator problem, thus fulfilling its motivating goal. It used hyperresolution rather than paramodulation, and made extensive use of weighting. It could also prove that subgroups of index 2 are normal and that Boolean rings are commutative, again without using paramodulation, although demodulation played an important role. These problems remain difficult today for many systems.