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,