AUTOMATED THEOREM PROVING
9
are generated. Since their conjunction is contradictory, the origi-
nal formula is unsatisfl.able.
The logic is one of extreme
si~plicity
and, with unificatipn,
power. However, clauses accumulated at a rapid rate. The elegant
simplicity of resolution led many researchers to invest time in
try-
ing to find restrictions and strategies of resolution to control the
explosive clause growth and to provide resolution deduction for-
mats amenable to heuristics for trimming clause growth. To even
name all the refinements of resolution is beyond reason here (the
appendix of Loveland [Lo5] summarizes twenty-five variations;
more exist). We settle for naming some of the variations that have
held continued interest beyond the 1965-1970 period when most
variations were proposed. Figure 2 names the variations we sum-
marize here. Of course, any short list must do injustice to useful
variants omitted; for this we can only apologize.
The variants we consider here are complete proof procedures
unless otherwise stated; that is, every unsatistiable formula has a
refutation within the proper format. By a
restriction of resolution
we mean a variant for which some clauses generated by the basic
resolution procedure are not generated; a
strategy of resolution
only rearranges the order of generation to get likely useful
clauses earlier. A
refinement of resolution
is either a restriction
or a
strateg~.
Recall that formulas are tested for unsatisfiability
by resolution, that conjunctive normal form is used and that all
quantifiers are removed by a process that involves the use of
"Skolem functions". (See Chang and Lee [CLl] or Loveland [Lo5].)
Several refinements of resolutions are important because they
are used within the successful theorem provers of Wos
et
a.l.
to be
mentioned later (and considered in the Wos and Winker paper in
this volume).
Un.it
preference,
one of the earliest refinements, is a
strategy favoring one-literal clauses. This guarantees that the
Previous Page Next Page