Linear Input (binary) Resolution

Given an input set of clauses and a clause C1 chosen from the input set, a linear input 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 chosen from the input set, by binary resolution. For any Ci, the centre clauses C1 to Ci-1 are the ancestor clauses of Ci.

Example
S5 = { ~p(Z),
       q(a,b),
       r(d),    (Top clause)
       p(Y) | ~r(X) | ~q(Y,X),
       p(Y) | ~r(X) | ~s(Y,X),
       s(c,d) }

Linear input deduction is complete for input sets of Horn clauses [Henschen & Wos, 1974], but is not complete for input sets that contain non-Horn clauses. Ringwood [1988] provides an interesting synopsis and references for the history of linear input deduction systems. Practical notes:

Example
S5 = { ~p(Z),
       q(a,b),
       r(d),
       p(Y) | ~q(Y,X) | ~r(X),
       p(Y) | ~s(Y,X) | ~r(X),
       s(c,d) }

Center clauses Side clauses
~p(Z) + p(Y) | ~q(Y,X) | ~r(X)
= ~q(Z,X) | ~r(X) + q(a,b)
= ~r(b) + Backtrack
= ~p(Z) + p(Y) | ~s(Y,X) | ~r(X)
= ~s(Z,X) | ~r(X) + s(c,d)
= ~r(d) + r(d)
= FALSE

Example
S7 = { ~r(X) | ~t(X),
       r(a) | ~p(S) | ~q(S),
       p(a),
       p(b),
       q(b),
       t(X) | ~p(a) }

Prolog is linear input resolution using a negative top clause, adding the side clause literals on the left, and a depth first search choosing the left most literal of the centre clause at each step.

Example
The set S7 would be written as a Prolog program:
r(a):-
    p(S),
    q(S).

p(a).

p(b).

q(b).

t(X):-
    p(a).
and a query at the Prolog prompt:
?- r(X),t(X).

Example
SN = { ~p(b,X) | ~q(X),
       r(a),
       ~q(X) | r(X),
       r(b) | ~q(c),
       p(b,a) | ~r(a),
       p(Y,c) | ~r(Y),
       q(c) }

Example
The set SN would be written as a Prolog program:
r(a).

r(X):-
    q(X).

r(b):-
    q(c).

p(b,a):-
    r(a).

p(Y,c):-
    r(Y).

q(c).
and a query at the Prolog prompt:
?- p(b,X),q(X).


Exam Style Questions

  1. Use linear-input resolution to derive the empty clause from the set
    S = { ~r(Y) | ~p(Y),
          p(b),
          r(a), 
          p(S) | ~p(b) | ~r(S),
          r(c) }