Linear Resolution

Given an input set of clauses and a clause C1 chosen from the input set, a linear deduction of Cn from the input set, with top clause C1, is a sequence of centre clauses C1,...,Cn. Each deduced clause Ci+1, i = 1..n-1, is deduced from the centre clause Ci and a side clause. The side clauses are the input set and C1,...,Ci-1. For any Ci, the centre clauses C1 to Ci-1 are the ancestor clauses of Ci. Refutations are written in a linear style.

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) }

Center clauses Side clauses
p(X) | l(X) | q + ~q | l(Y)
= p(X) | l(X) | l(Y) + ~l(Z) | ~m(S) | r(Z)
= p(X) | ~m(S) | r(X) + ~r(b) | ~l(T) | ~s(b)
= p(b) | ~m(S) | ~l(T) | ~s(b) + s(b)
= p(b) | ~m(S) | ~l(T) + p(X) | l(X) | l(Y)
= p(X) | p(b) | ~m(S) + m(a) | r(b)
= p(X) | p(b) | r(b) + ~r(b) | ~l(T) | ~s(b)
= p(X) | p(b) | ~l(T) | ~s(b) + s(b)
= p(X) | p(b) | ~l(T) + p(X) | l(X) | l(Y)
= p(X') | p(b) | p(X) + ~p(b)
= FALSE

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:

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) }

Center clauses Side clauses
p(Z) | q(Z) + ~q(a)
= p(a) + ~p(X) | t(X)
= t(a) + Backtrack
= p(a) + ~p(X) | s(X)
= s(a) + Backtrack
= p(Z) | q(Z) + ~q(T) | s(T)
= p(Z) | s(Z) + ~s(b) | m(W)
= p(b) | m(W) + ~s(b) | ~m(a)
= p(b) | ~s(b) + p(Z') | s(Z')
= p(b) | p(b) + ~p(X) | t(X)
= t(b) + ~t(b) | p(b)
= p(b) + Backtrack
= t(b) + ~t(b) | s(b)
= s(b) + ~s(b) | ~m(a)
= ~m(a) + ~s(b) | m(W)
= ~s(b) + s(b)
= FALSE

Completeness by Construction

Any normal refutation can be converted to a linear refutation. Consider the proof tree from this example.

Example
S4a = { ~p(b),
        p(X) | l(X) | q,   (Top clause)
        ~q | l(Y),
        ~l(Z) | r(Z),
        ~r(b) | ~l(T) }

p(X) | l(X) | q + ~q | l(Y)
= p(X) | l(X) | l(Y)
~l(Z) | r(Z) + ~r(b) | ~l(T)
= ~l(b) | ~l(T)
p(X) | l(X) | l(Y) + ~l(b) | ~l(T)
= p(b)
p(b) + ~p(b)
= FALSE

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].


Linear Binary Resolution

In a linear refutation, any centre clause literals that are involved in a genuinely full resolution (i.e., 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) }

Center clauses Side clauses
p(X) | l(X) | q + ~q | l(Y)
= p(X) | l(X) | l(Y) + ~l(Z) | ~m(S) | r(Z)
= p(X) | l(X) | ~m(S) | r(Z) + ~r(b) | ~l(T) | ~s(b)
= p(X) | l(X) | ~m(S) | ~l(T) | ~s(b) + s(b)
= p(X) | l(X) | ~m(S) | ~l(T) + p(X') | l(X') | l(Y)
= p(X') | l(X') | p(X) | l(X) | ~m(S) + Factoring
= p(X) | l(X) | ~m(S) + m(a) | r(b)
= p(X) | l(X) | r(b) + ~r(b) | ~l(T) | ~s(b)
= p(X) | l(X) | ~l(T) | ~s(b) + s(b)
= p(X) | l(X) | ~l(T) + p(X) | l(X) | l(Y)
= p(X') | l(X') | p(X) | l(X) + Factoring
= p(X) | l(X) + ~l(Z) | ~m(S) | r(Z)
= p(X) | ~m(S) | r(X) + ~r(b) | ~l(T) | ~s(b)
= p(b) | ~m(S) | ~l(T) | ~s(b) + s(b)
= p(b) | ~m(S) | ~l(T) + p(X) | l(X)
= p(X) | p(b) | ~m(S) + Factoring
= p(b) | ~m(S) + m(a) | r(b)
= p(b) | r(b) + ~r(b) | ~l(T) | ~s(b)
= p(b) | ~l(T) | ~s(b) + s(b)
= p(b) | ~l(T) + p(X) | l(X)
= p(X) | p(b) + Factoring
= p(b) + ~p(b)
= FALSE

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) }