Tableaux Refinements

Connection Tableaux

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

Center clauses Side clauses Center chains Side chains
p(X) | l(X) | q + ~q | l(a) p(X) l(X) q + ~q l(a)
= p(X) | l(X) | l(a) + ~l(a) | r = p(X) l(X) [q] l(a) + ~l(a) r
= p(X) | l(X) | r + ~r | ~l(Z) = p(X) l(X) [q] [l(a)] r + ~r ~l(Z)
= p(X) | l(X) | ~l(Z) + p(X) | l(X) | l(a) = p(X) l(X) [q] [l(a)] [r] ~l(Z) + Reduction
= p(X) | l(X) | p(X') | l(X') + Factoring = p(X) l(X) [q] [l(a)] [r] + Truncation
= p(X) | l(X) + ~l(a) | r = p(X) l(X) + ~l(a) r
= p(a) | r + ~r | ~l(Z) = p(a) [l(a)] r + ~r ~l(Z)
= p(a) | ~l(Z) + p(X) | l(X) = p(a) [l(a)] [r] ~l(Z) + Reduction
= p(a) | p(X) + Factoring = p(a) [l(a)] [r] + Truncation
= p(a) + ~p(a) = p(a) + ~p(a)
= [p(a)] + Truncation
= FALSE = FALSE

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.

Tableaux

A tableau is a tree of literals. Each leaf literal in a tableau is classified as either open or closed. The disjunction of the open literals in a tableau make up the clause that is represented by the tableau. A closed tableau corresponds to a refutation.

Notation :

Core operations

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.

Admissbility restrictions

Common admissibility restrictions are :

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