10
D.W. LOVELAND
resolvent is shorter than the ionger parent clause, clearly
beneficial when one seeks two one-literal clauses of complemen-
tary literals to conclude t11e proof. This strategy was introduced
in Was, Robinson and Carson [WCl].
A resolution restriction also introduced in Was, Robinson and
Carson [WCl] is the set-of-support restriction. A support set T, a
subset of the set S of all the given clauses, is chosen and then two
clauses from
S- T
are never resolved together. This means that
every resolvent has in its deduction history some clause of T. T is
usually chosen to be (a subset of) the clauses special to the prob-
lem at hand.
Hyperresolution (see Robinson [Ro2]), also used by Wos et at.,
in its original form restricts resolutions to where one parent
clause contains only positive literals (i.e. atomic formulas) and
any resolvent containing a negative iiteral is immediately used in
all permitted resolutions and then discarded. There now exist a
number of important generalizations and variants of this restric-
tion. The three refinements discussed all appeared within the first
year of the introduction of resolution.
A proof procedure called model elimination (see Loveland
[Lol], [Lo2]) appeared about the same time. It is not a resolution
procedure but is close to a very restricted form of linear resolu-
tion,
which was not defined until several years later (and intro-
duced simultaneously in Loveland [Lo3] and Luckham [Lul],
back-to-back at a 1968 conference). Linear resolution has each
resolution of a deduction use the preceding clause of. the deduc-
tion as one parent clause. One views the deduction as a series of
modifications to the first clause, since (usually) only one literal is
dropped and perhaps some added when passing from one clause to
the next. (This ignores any further instantiation effect of a substi-
tution.) Kowalski and Kuehner [KKl] provided the translation of
Previous Page Next Page