Example | ||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S8 = { p(X) | l(X) | q, (top clause) ~q | l(Y), ~l(Z) | ~m(S) | r(Z), ~r(b) | ~l(T) | ~s(b), s(b), m(a) | r(b), ~p(b) }
|
Note the duplicated steps (which will be dealt with by refinements).
Example |
---|
S9 = { ~p(X) | ~q(X,b), (Top clause) ~s(W) | q(W,W), p(b), q(Y,T) | r(T) | s(Y), ~r(Z) | s(X) } |
Practical Notes:
CL|
are all within a separate subtree of the
normal resolution proof.
A common selection is the right most literal, and to place new side
clause literals to the right so that they are dealt with first.
Example | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S6 = { p(Z) | q(Z), ~p(X) | t(X), ~p(X) | s(X), ~t(b) | p(b), ~t(b) | s(b), ~s(b) | m(W), ~s(b) | ~m(a), ~q(a), ~q(T) | s(T) }
|
Example | ||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S4a = { p(X) | l(X) | q, (Top clause) ~q | l(Y), ~l(Z) | r(Z), ~r(b) | ~l(T), ~p(b) }
|
The linearisation proceeds as follows.
Choose any leaf of the proof tree.
This clause becomes the top clause of the linear refutation.
Follow the refutation down until a resolution with a non-input clause is
found.
Call the centre clause at that point C|
and the other
clause S|
.
Call the resolved upon literals from the centre clause
CL|
, and the resolved upon literals from the
non-input clause SL|
.
Find one of the originals from SL|
in a leaf
in the subtree; call it Ls
.
Recursively linearise the sub-refutation from that leaf down to the non-input
clause.
That linearised sub-refutation is then inserted under
C|
.
This will leave the literals SL|-Ls
in the resultant centre clause.
An ancestor resolution against the literals CL|
in C|
will get to the resolvant (possibly with
some literals inherited from C|-CL|
-
they are collapsed in the next resolution step or can be factored away)
below the point where the non-input clause is used in the original refutation.
In the above example, choose p(X) | l(X) | q
as the
initial leaf.
The refutation is followed down from p(X) | l(X) | q
to the
resolution
between C|
= p(X) | l(X) | l(Y)
and S|
= ~l(b) | ~l(T)
.
CL|
= l(X) | l(Y)
and
SL|
= ~l(b) | ~l(T)
.
The subtree to be linearised is
Choosing Ls
= ~l(Z)
in
~l(Z) | r(Z)
, this linearises trivially to
which is then inserted after the initial linear segment, to get
An ancestor resolution with p(X) | l(X) | l(Y)
is then
needed to remove SL|-Ls
=
~l(T)
from p(b) | ~l(T)
.
Note the extra C|-CL|
= p(X)
that is introduced.
Any extra literals in C|-CL|
subsume
literals inherited from the ancestor clause.
The extra literals in C|-CL|
"subsume"
the inherited ones because the inherited ones may have become instantiated
in the subdeduction between the ancestor and the ancestor resolution.
So p(X)
subsumes the p(b)
inherited from
p(X) | l(X) | l(Y)
, and can thus be resolved upon at the
same time as the inherited one.
Alternatively the extra ancestor literals can be factored out.
Linear resolution is refutation complete.
Proof |
---|
By the construction above [Luckham 1970, discovered 1968]. |
CL|
contains
more than one literal) with an input side clause, can resolved upon
individually using binary resolution and duplicating the steps required.
Let the resolved upon literal of CL|
be
Lc
.
If binary resolution is used in the ancestor resolution steps, then
all the literals C|-Lc
from the
ancestor clause will be in the resolvant.
As before, these literals subsume the inherited copies, and can be factored
out. In the above example:
Any extra literals from side clauses that are involved in full resolution steps can be dealt with by ancestor resolving with the parent centre clause (either immediately or later), and factoring the duplicated literals from the centre clause. The immediate case happens naturally as part of linearization, as shown in this extract from the linearization of example S4.
Thus linear resolution is refutation complete using binary resolution and 'compulsory' factoring of extra literals after ancestor resolution steps. The ancestor resolution and the following factoring will always shorten the centre clause.
Example | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S8 = { p(X) | l(X) | q, (top clause) ~q | l(Y), ~l(Z) | ~m(S) | r(Z), ~r(b) | ~l(T) | ~s(b), s(b), m(a) | r(b), ~p(b) }
|
Note the duplicated duplicated (not a typo) steps (which will be dealt with by refinements).
Example |
---|
S9 = { ~p(X) | ~q(X,b), (top clause) ~s(W) | q(W,W), p(b), q(Y,T) | r(T) | s(Y), ~r(Z) | s(X) } |