12
D.W. LOVELAND
as we consider later. A Horn forniula in conjunctive normal form
has at most one positive literal per clause, but as many negative
literals as desired.
Associated with resolution procedures is a means for handling
equality called
paramodulation
by Wos and G. Robinson (see
[WR2]). In essence this is the equality replacement rule with
unification; it replaces all equality axioms except· certain
reflexivity axioms for functions. The term
demodulation
is used
when paramodulation is restricted to replacement of the (usually)
shorter term by the longer term with no instantiation allowed in
the formula incorporating the replacement (see [WRl]). Paramo-
dulation and demodulation continue to play a very important role
in AURA, a replacement resolution theorem prover now used by
Wos
et al.
at Argonne National Labs. We discuss AURA later.
The above refinements are discussed in detail in Chang and
Lee [CLl] or Loveland [Lo5].
It is interesting to note that a proof procedure very close to
resolution in spirit (given as a test for validity rather than
unsatisfiability) was invented by Maslov in the USSR almost simul-
taneously with Robinson's invention of resolution. The original
work (Maslov [Mal]), called the
inverse
method, is reviewed
together with resolution by Maslov [Ma2]; also see Kuehner [Kul]
for a direct comparison of resolution and the inverse method of
Maslov.
One of the earliest and certainly the most successful of inves-
tigators to implement a resolution system is Larry·Wos, one of the
recipients of the first ATP prizes. We shall comment later on his
long term development of resolution provers but the reader is
advised to also see the paper in this volume.
While the logic approach received much of the attention in the
early sixties and certainly most of the attention in the late sixties,
Previous Page Next Page