8

D.W. LOVELAND

The three years around 1960 ·was a significant time for the

logic approach to ATP. One more notable event occurred at this

time. In 1960 Dag Prawitz published a paper attacking the all-

too-apparent major problem with the D-P procedure, the

enumeration of substitutions (see Prawitz [Pr1]). Prior to this

point substitutions were determined by some enumeration scheme

that covered every possibility. Prawitz realized that the only

important substitutions create complementary literals. Prawitz

found substitutions by deriving a set of identity conditions (equa-

tions) that will lead to contradictory propositional formula if the

conditions are met. The insight was profound but the implementa-

tion awkward. Davis later combined the idea with the D-P pro-

cedure to realize the advantages of both (see Davis [Dal]).

The idea of matching found its cleanest formulation in the

resolution principle put forth by J.A." Robinson (1965) (see Robin-

son [Rol]). The logic formulated by Robinson had no logical

axioms and one inference rule that employed a substitution device

called unification. The inference rule is as follows: if A v L

1

and

B

v-

La

are variable-disjoint clauses

(A

and

B

are disjunctions of

literals;

L

1

and

La

are literals) then from

A

v

l

1

and

B

v-

La

(the

parent clauses) deduce clause A17 v B17 (the resolvent) where 17 is

a substitution such that l 117

=

1217. The propositional part of this

inference rule is essentially the cut rule of Gentzen [Ge2], a gen-

eralization of

modus

ponens. The substitution 17 is special in that

it is the most general substitution that allows the equality to hold.

Thus any substitution that would identify these two literals is an

instance of this substitution. This is a powerful tool because it

eliminates branching of search due to different possible substitu-

tions that equate these two atoms but lead to different clauses.

One uses the resolution inference rule to generate clauses (with

some pruning possible) until for some literal

L,

literals

l

and ,.,.

L