AUTOMATED THEOREM PROVING
11
model elimination into a very restricted linear resolution format
(also done independently in Loveland [Lo4]). Their procedure,
called Slrresolution, was used by several people in theorem prov-
ing projects, and by Colmerauer and Roussel in an early version of
Prolog, a programming language we discuss later. Perhaps the
primary importance of the model elimination procedure itself is in
the MESON format, where it provides a natural completion to the
problem reduction format (see Loveland and Stickel [LS2], Love-
land [Lo5]). The problem reduction format is as old as the field
itself, and probably is in its purest form in the Geometry
Theorem-proving Machine discussed earlier. The problem reduc-
tion format is associated with "natural inference systems", con-
sidered later. (For a totally different completion of a problem
reduction format see Plaisted [Pll].)
A number of resolution refinements (including variants of
model elimination) allow literals in clauses to be ordered to reduce
multiple derivations of the same clause. The strongest ordering
restrictions were based on the method called Loclcing (Boyer [Bol])
which allows a unique integer assignment to each literal
occurrence of each input clause. Resolution need be done using
only the lowest indexed integer of each clause. This does not allow
complete freedom of order assignment for each resolvent (without
endangering completeness) but is very close to that .. This powerful
ordering property still has its adherents (e.g., see Sandford [Sal]).
Two important incomplete forms of resolution restrictions are
unit clause resolution and input clause resolution. The former
permits resolution only when one parent is a unit clause and the
latter is a restricted form of linear resolution where one parent is
always an input (given) clause. Chang [Chl] shows these pro-
cedures to be of equal power; indeed, they are complete over the
class of Horn formulas, a class receiving increased attention lately
Previous Page Next Page