In the chain format refinements, the chosen B-literal always comes from
the rightmost cell of the centre chain.
This ensures that the literals C|-Lc
of the ancestor clause are available for factoring when an ancestor resolution
is implemented by reduction.
The A-literals against which reduction takes place are discarded when
the deduction that removes Lc
(corresponding to a
completed linearisation of a subtree in a normal deduction) is completed.
After that point one of C|-Lc
in the
current centre chain is resolved upon, and is no longer available for
factoring away ancestor literals introduced by reduction.
Consider the linear binary resolution and corresponding ME refutation:
Example | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S4z = { ~p(a), p(X) | l(X) | q, ~q | l(a), ~l(a) | r, ~r | ~l(Z) }
|
In the linear binary version, it is important that the ancestor resolution
using p(a) | ~l(Z)
is against p(X) | l(X)
,
because the p(X)
from the ancestor can factor against the
p(a)
. If the ancestor p(X) | l(X) | l(a)
were used, the l(X)
from the ancestor would not be able to
factor away.
In the ME version, this constraint is implemented by truncating the A-literal
[l(a)]
(the first one) before extending against the
l(X)
.
Although it is thus reasonable to ignore other centre chain literals once
one has been selected for attention (the AND decision), it is not
necessary to do so.
It is possible to start "working on" another center chain literal,
provided that the A-literals created are "kept separate", so that
reduction steps take place only against A-literals that represent ancestor
clauses whose literals can be factored away after an ancestor resolution.
In the above example extension against, e.g., l(X)
is
possible, provided that the A-literal created is not used for reducing
the (first) ~l(Z)
.
Tableau refinements make this possible.
This is one way of looking at the tableau refinements of resolution. However, these refinements were discovered independently of the linear refinements [REF], and the relationship between the two noticed only later.
Notation :
Initialization selects a top clause for the tableau, and makes the literals of the clause the open leaves of a root node.
Extension resolves an open literal against a literal in an input clause. The deduced tableau is formed by
Reduction unifies an open literal with a complementary internal literal above it in the tableau. The deduced tableau is formed by marking the open literal as closed.
Example |
---|
S4 = { ~p(b), p(X) | l(X) | q, (top clause) ~q | l(Y), ~l(Z) | ~l(S) | r(Z), ~r(b) | ~l(T) } |
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) } |