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