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.
Previous Page Next Page