AUTOMATED THEOREM PROVING 7

interest was Wang's later attention . to pattern analysis to over-

come the explosion of formulae that resulted from enumerating

all possible substitutions of terms for quantified variables. This

anticipated somewhat the matchi~g technique of Prawitz (see

below) but also suggested heuristic exploration with shades of AI

techniques.

The straightforward approach taken by Gilmore made his

theorem prover a target for improvement. One of the most suc-

cessful was the procedure introduced by Martin DaVis and Hilary

Putnam (see Davis, Putnam [DPl]). The D-P procedure (1960)

greatly reduced the propositional processing. The question of

validity of a predicate calculus formula can be reduced to a series

of validity questions about ever-expanding propositional formulas.

Herbrand's Theorem states that to each valid first-order formula

C

there is a propositional formula

C

1

v C2 v

C3

v · · · v

C,.

(truth-functionally) valid

if C

is valid. The

q

are essentially sub-

stitution instances over an expanded term alphabet of

C

with

quantifiers removed. Thus one could test

C

1

v C2 v

C3

v · · · v

q,

for ever-increasing i, by truth tables

if

one wished, and could pro-

claim the original a theorem if a tautology was shown to exist.

Truth tables happen to be quite inefficient. The D-P procedure

actually sought unsatisfiable formulas (the dual of the validity

problem) and worked with conjunctive normal form (cnf form).

Cnf form is a conjunction of

cla.u.ses,

each clause a disjunction of

liter.a.ls,

atomic formulas (atoms) or their negations. The D-P pro-·

cedure made optimal use of simplification by cancellation due to

one-literal clauses or because some literals might not have their

complement (the same atomic formula, but only one with a nega-

tion sign) in the formula. A simplified formula was

split

into two

formulas so further simplification could recur anew.