Automated Theorem Proving: Clauses, Unification, Equality, and Search

First-order validity is undecidable, but that does not prevent a program from finding proofs. A complete effective proof calculus permits systematic enumeration: valid formulas eventually receive proofs, while some invalid inputs may leave the search running indefinitely.

Practical automated theorem proving asks how to organize that search well enough to solve useful problems. Its history concerns representation, inference, redundancy, and heuristics as much as the existence of an algorithm.

Early procedures and early machines

Jacques Herbrand's 1930 work connected first-order reasoning with finite combinations of substitution instances. Later researchers turned related ideas into increasingly practical procedures.

The Logic Theorist, developed by Allen Newell, J. C. Shaw, and Herbert Simon in the 1950s, searched for proofs in propositional mathematics. Its historical importance includes the use of heuristic organization and its role in early artificial intelligence.

Martin Davis and Hilary Putnam's 1960 procedure belongs to another important line. It reduced logical problems to systematic operations on clauses, helping establish the path toward propositional satisfiability procedures.

John Alan Robinson's 1965 resolution paper combined a powerful inference rule with unification. The combination made it possible to reason with variables directly rather than enumerate every ground substitution in advance.

These systems differed in scope and strategy. A single label such as “machine proof” can conceal those differences.

Clauses and refutation

A literal is an atomic formula or its negation. A clause is a disjunction of literals, conventionally with its variables understood as universally quantified.

To prove that premises imply a goal, a refutation procedure adds the negation of the goal and seeks a contradiction.

Consider the premises

and the desired conclusion $\exists x\,Q(x)$.

Negating the conclusion gives $\forall x\,\neg Q(x)$. Eliminating the existential premise introduces a fresh Skolem constant $c$. The resulting clausal problem is

The constant denotes a witness in an expanded language. Skolemization preserves satisfiability in the appropriate sense: a model of the original existential statement can be expanded by choosing a witness, and a model of the Skolemized statement gives a model of the original statement after forgetting the new symbol.

It is not literal equivalence between formulas in the original language. When an existential depends on preceding universal variables, a Skolem function rather than a single constant is needed.

A complete resolution calculation

Resolve

with $P(c)$ using the substitution $x:=c$. The complementary literals cancel, leaving $Q(c)$.

Resolve $Q(c)$ with $\neg Q(y)$ using $y:=c$. No literals remain. The result is the empty clause, representing falsity.

Every inference preserves the relevant consequence relation. The contradiction shows that the premises together with the negated goal are unsatisfiable; therefore the original conclusion follows.

This small example displays the whole architecture: normalize the problem, identify complementary literals, compute substitutions, and derive a refutation.

Larger problems introduce choices at every stage. Which clauses should be combined? Which literals should be selected? Which consequences are redundant? Those choices determine whether a mathematically complete method is computationally useful.

What unification contributes

Unification finds substitutions making expressions identical.

For instance, unifying

requires $x:=a$ and $y:=b$.

A most general unifier leaves as much freedom as possible: every other unifier is an instance of it, in the standard sense. “Most general” does not mean the substitution with the fewest printed symbols.

The occurs check prevents an invalid finite-term solution to an equation such as

No finite first-order term can equal a proper term containing itself. Some programming systems deliberately support cyclic or rational trees, but that changes the term domain and must be accounted for explicitly.

Unification allows one inference with variables to represent a family of ground inferences. It thereby converts a foundational existence theorem into a more economical computational method.

Herbrand's theorem and fairness

For an unsatisfiable set of first-order clauses in the usual Skolemized setting, Herbrand's theorem yields a finite unsatisfiable collection of ground instances. If the language has no ground term, one may add a fresh constant for the construction.

The theorem does not say that there is a small instance collection, or that an arbitrary enumeration will reach the right instances promptly.

Resolution's refutational completeness, with the appropriate treatment of factoring and the calculus's other requirements, shows that an unsatisfiable clause set has a resolution refutation. A search implementation must avoid indefinitely neglecting every route to such a refutation.

Fairness conditions make that requirement precise. Practical provers also use resource limits, selection policies, and incomplete modes. Failure to find a proof under those limits is not a proof that the conjecture is false.

Equality requires additional organization

Suppose we know $a=b$ and $P(a)$. We want $P(b)$.

One approach adds general equality axioms to an ordinary first-order prover. This is logically possible but can create a large and poorly directed search.

Paramodulation, associated with George Robinson and Larry Wos, incorporates replacement using equalities into the inference machinery. The example then becomes a direct replacement at the occurrence of $a$.

The distinction between George Robinson and John Alan Robinson matters here: their contributions are often compressed into a single surname.

Term rewriting orients suitable equations as directed simplification rules. Knuth–Bendix completion, introduced in 1970, attempts to turn equations into a convergent rewriting system by resolving conflicts between reductions.

Completion can fail to terminate or encounter orientation difficulties. Its success depends on the equational theory and the chosen ordering; it is not a general decision procedure for all equations.

Superposition calculi, developed through work including Leo Bachmair and Harald Ganzinger, combine ordered equality reasoning with restrictions that control redundant inferences. This line became central to strong first-order provers with equality.

The Robbins problem

Herbert Robbins asked whether a particular equational axiom system already characterized Boolean algebras. The problem resisted substantial mathematical work.

In October 1996, William McCune's EQP found a proof establishing the needed result. The proof used earlier mathematical reductions, including work by Stephen Winker, and specialized equational reasoning.

McCune's project record preserves the input, proof, and program. The successful search established a Winker condition whose known consequence was that every Robbins algebra is Boolean.

The case illustrates a division of labor. Human work formulated the question, developed intermediate criteria, designed the prover, and configured the search. The machine found a particular formal derivation. Subsequent checking and mathematical exposition assessed and communicated the result.

It was a substantive mathematical discovery, but it does not show that general proof search had become easy or that every automated proof has the same architecture.

Discovery and checking

A search program may contain complicated heuristics, indexing structures, and optimization code. A proof object or derivation trace can sometimes be checked by a simpler independent procedure.

This separation reduces the amount of search machinery that must be trusted for a particular conclusion. The checker must still implement the intended rules correctly, and the input must accurately formalize the theorem.

The distinction will recur in SAT certificates, proof assistants, and learned theorem proving. A method for proposing a proof and a method for accepting it need not be the same program.

The next computational limit

Undecidability explains why unrestricted first-order proof search cannot always decide its input. Even decidable reasoning tasks can require enormous resources. Propositional satisfiability exposes that second difficulty particularly clearly.

Sources and further reading

• Jacques Herbrand, Recherches sur la théorie de la démonstration (1930).
• Allen Newell, J. C. Shaw, and Herbert A. Simon, “Empirical Explorations with the Logic Theory Machine” (1957).
• Martin Davis and Hilary Putnam, “A Computing Procedure for Quantification Theory” (1960).
• J. Alan Robinson, “A Machine-Oriented Logic Based on the Resolution Principle” (1965).
• George Robinson and Larry Wos, “Paramodulation and Theorem-Proving in First-Order Theories with Equality” (1969).
• Donald E. Knuth and Peter B. Bendix, “Simple Word Problems in Universal Algebras” (1970).
• Leo Bachmair and Harald Ganzinger, “Resolution Theorem Proving” (2001).
• William McCune, “Solution of the Robbins Problem” (1997), with proof artifacts and the 1996 discovery record.