Linear Input Resolution

Linear Input (binary) Resolution

Given an input set of clauses and a clause C₁ chosen from the input set, a linear input deduction of C_n from the input set, with top clause C₁, is a sequence of centre clauses C₁,...,C_n. Each deduced clause C_i+1, i = 1..n-1, is deduced from the centre clause C_i and a side clause chosen from the input set, by binary resolution. For any C_i, the centre clauses C₁ to C_i-1 are the ancestor clauses of C_i.

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

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:

If a refutation exists, one exists with one of the negative clauses as top clause. Thus it's safe to try only each of the negative clauses as top clauses.
If the top clause is negative, then all center clauses are necessarily negative, and only positive literals in each mixed or positive clause can be resolved against at each step.
The selection of which centre clause literal to resolve upon is an AND decision, and can be committed to once made. A common selection is the right most or left most literal.
The new literals from the side clauses can be merged with the remaining centre clause literals in any way. A common way is to add them to the right or the left.
During a linear deduction, it is necessary to allow for alternative side clauses at each step. One way to implement this is via backtracking.

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

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

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

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