Chain Format Linear Refinements

It was noted in the section on linear resolution that in an ancestor binary resolution the ancestor literals that are not resolved upon subsume the corresponding ones that are inherited through the linear steps, and can therefore be factored out. The chain format linear resolution systems take advantage of this knowledge, and simply records the existence of L^c and leave C^|-L^c implicit, secure in the knowledge that the literals C^|-L^c can be factored away when an ancestor resolution is performed. These recorded literals, called A-literals, are discarded when the deduction that removes L^c (corresponding to a completed linearisation of a subtree in a normal deduction) is completed, after which one of C^|-L^c is necessarily resolved upon and is no longer available for factoring. The chain format systems also use the ability to ignore other centre chain literals once one has been selected for attention (the AND decision).

Chains

A chain is an ordered sequence of literals. Each literal in a chain is classified as either an A-, B-, or C-literal. The disjunction of the B-literals in a chain makes up the clause that is represented by the chain. An uninterrupted sequence of B-literals in a chain is called a cell. Input clauses are used to form input chains which consist entirely of B-literals. Chains that contain a single B-literal are called unit chains. Centre clauses of linear deductions are represented by centre chains. Centre chains may contain A-, B- and C-literals. Various items of information can be associated with the literals in a chain.

Notation :

• A-literals are placed in rectangles.
• B-literals stand free.
• C-literals are placed in ellipses.
• Literals in a chain are simply separated by spaces (the | is omited).

Core operations

All chain format linear deduction systems have a common core of deduction operations. There are two inference operations based on binary resolution and one bookkeeping operation. The inference operations are extension and reduction.

Extension resolves a B-literal in the rightmost cell of a centre chain against a B-literal in an input chain. The deduced chain is formed by

• Placing the resolved upon centre chain B-literal at the right-hand end of the centre chain and reclassifying it as an A-literal
• Adding the non-resolved upon input chain B-literals to the right of the new A-literal.

Reduction unifies a B-literal in a centre chain with a complementary A-literal to its left. The deduced chain is formed by removing the B-literal from the centre chain. Reduction implements ancestor resolution, followed by a sequence of factoring operations. The reduction of a B-literal against the A-literal immediately to its left may also be viewed as factoring of the corresponding input chain.

The bookkeeping operation is truncation (also called contraction). Truncation removes an A- or C-literal from the right-hand end of a centre chain. In some deduction systems, the truncation of an A-literal may cause the insertion of another A- or C-literal.

The Model Elimination (ME) Procedure

Example

S4 = { ~p(b), p(X) | l(X) | q, (top clause) ~q | l(Y), ~l(Z) | ~l(S) | r(Z), ~r(b) | ~l(T) } Center clauses Side clauses | Center chains Side chains p(X) | l(X) | q + ~q | l(Y) | p(X) l(X) q + ~q l(Y) = p(X) | l(X) | l(Y) + ~l(Z) | ~l(S) | r(Z) | = p(X) l(X) [q] l(Y) + ~l(Z) ~l(S) r(Z) = p(X) | l(X) | ~l(S) | r(Y) + ~r(b) | ~l(T) | = p(X) l(X) [q] [l(Y)] ~l(S) r(Y) + ~r(b) ~l(T) = p(X) | l(X) | ~l(S) | ~l(T) + p(X') | l(X') | l(Y) | = p(X) l(X) [q] [l(b)] ~l(S) [r(b)] ~l(T) + Reduction = p(X) | l(X) | ~l(S) | p(X') | l(X') + Factoring | = p(X) l(X) [q] [l(b)] ~l(S) [r(b)] + Truncation = p(X) | l(X) | ~l(S) + p(X') | l(X') | l(Y) | = p(X) l(X) [q] [l(b)] ~l(S) + Reduction = p(X) | l(X) | p(X') | l(X') + Factoring | = p(X) l(X) [q] [l(b)] + Truncation = p(X) | l(X) + ~l(Z) | ~l(S) | r(Z) | = p(X) l(X) + ~l(Z) ~l(S) r(Z) = p(X) | ~l(S) | r(X) + ~r(b) | ~l(T) | = p(X) [l(X)] ~l(S) r(X) + ~r(b) ~l(T) = p(b) | ~l(S) | ~l(T) + p(X) | l(X) | = p(b) [l(b)] ~l(S) [r(b)] ~l(T) + Reduction = p(b) | ~l(S) | p(X) + Factoring | = p(b) [l(b)] ~l(S) [r(b)] + Truncation = p(b) | ~l(S) + p(X) | l(X) | = p(b) [l(b)] ~l(S) + Reduction = p(b) | p(X) + Factoring | = p(b) [l(b)] + Truncation = p(b) + ~p(b) | = p(b) + ~p(b) | = [p(b)] + Truncation = FALSE | = FALSE

Practical Notes:

• Each of the chain format linear deduction systems can use admissibility restrictions to reject some centre chains. Common admissibility restrictions are :
  • No two non-B-literals have identical atoms (in a loop, or should have reduced).
  • No A- or C-literal is to the left of an identical B-literal (in a loop).
  • No B-literal is complementarily identical to another B-literal in the same cell, or to the A-literal immediately to the right of the cell (a tautology has been used).
  • No A-literal is complementarily subsumed by a unit input chain, unless the A-literal is rightmost in the centre chain (should have extended).
• An ANL loop implementation places the input clauses in the CanBeUsed list, and a copy of the top chain in the ToBeUsed list. The ChosenClause is simply removed from the ToBeUsed list (not transferred to the CanBeUsed list). A special form of subsumption is required (I'VE GOT THE DETAILS SOMEWHERE (IMPLEMENTED AT LEAST)).

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 chains Side clauses p(X) l(X) q + ~q l(Y) = p(X) l(X) [q] l(Y) + ~l(Z) ~m(S) r(Z) = p(X) l(X) [q] [l(Z)] ~m(S) r(Z) + ~r(b) ~l(T) ~s(b) = p(X) l(X) [q] [l(b)] ~m(S) [r(b)] ~l(T) ~s(b) + s(b) = p(X) l(X) [q] [l(b)] ~m(S) [r(b)] ~l(T) [s(b)] + Truncate = p(X) l(X) [q] [l(b)] ~m(S) [r(b)] ~l(T) + Reduce = p(X) l(X) [q] [l(b)] ~m(S) [r(b)] + Truncate = p(X) l(X) [q] [l(b)] ~m(S) + m(a) r(b) = p(X) l(X) [q] [l(b)] [~m(a)] r(b) + ~r(b) ~l(T) ~s(b) = p(X) l(X) [q] [l(b)] [~m(a)] [r(b)] ~l(T) ~s(b) + s(b) = p(X) l(X) [q] [l(b)] [~m(a)] [r(b)] ~l(T) [~s(b)] + Truncate = p(X) l(X) [q] [l(b)] [~m(a)] [r(b)] ~l(T) + Reduce = p(X) l(X) [q] [l(b)] [~m(a)] [r(b)] + Truncate = p(X) l(X) + ~l(Z) ~m(S) r(Z) = p(X) [l(X)] ~m(S) r(X) + ~r(b) ~l(T) ~s(b) = p(b) [l(b)] ~m(S) [r(b)] ~l(T) ~s(b) + s(b) = p(b) [l(b)] ~m(S) [r(b)] ~l(T) [~s(b)] + Truncate = p(b) [l(b)] ~m(S) [r(b)] ~l(T) + Reduce = p(b) [l(b)] ~m(S) [r(b)] + Truncate = p(b) [l(b)] ~m(S) + m(a) r(b) = p(b) [l(b)] [~m(a)] r(b) + ~r(b) ~l(T) ~s(b) = p(b) [l(b)] [~m(a)] [r(b)] ~l(T) ~s(b) + s(b) = p(b) [l(b)] [~m(a)] [r(b)] ~l(T) [~s(b)] + Truncate = p(b) [l(b)] [~m(a)] [r(b)] ~l(T) + Reduce = p(b) [l(b)] [~m(a)] [r(b)] + Truncate = p(b) + ~p(b) = [p(b)] + Truncate = FALSE

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

Problem - repeated deductions.

Linear resolution with Selection function (SL-resolution)

Factoring provides a mechanism by which two literals, that could possibly both be removed from the centre chain (proved to not be in any model of the input set) by the same sequence of deduction operations, are combined so that they can be removed simultaneously by a single subdeduction. SL-resolution avoids repeated deductions by using (m-)factoring.

Example

S4 = { ~p(b), p(X) | l(X) | q, (top clause) ~q | l(Y), ~l(Z) | ~l(S) | r(Z), ~r(b) | ~l(T) } p(X) l(X) q + ~q l(Y) = p(X) l(X) [q] l(Y) + Factoring = p(X) l(X) [q] + Truncation = p(X) l(X) + ~l(Z) ~l(S) r(Z) = p(X) [l(X)] ~l(S) r(X) + ~r(b) ~l(T) = p(b) [l(b)] ~l(S) [r(b)] ~l(T) + Reduction = p(b) [l(b)] ~l(S) [r(b)] + Truncation = p(b) [l(b)] ~l(S) + Reduction = p(b) [l(b)] + Truncation = p(b) + ~p(b) = [p(b)] + runcation = FALSE

The steps that are repeated in the simple ME proof are only performed once here, because the unifiable literals are factored. Factoring thus preempts the necessity for repeating the subdeduction, and results in a shorter refutation. The preemptive nature of factoring can be a disadvantage - it might be inappropriate or even impossible to remove both the literals using a single subdeduction. In the following example, this would be the case if ~p(a) were to be replaced by ~l(b) and ~p(b) in the input set. Unless the two factored literals are identical, it is necessary to permit the alternative of not factoring, i.e., a choice point must be established. This increases the size of the search space.

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

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

The ME Procedure with Lemmas

The truncation operation of the ME procedure includes a mechanism by which lemma chains can be produced and added to the input set. The literals that consitute a lemma chain are determined from integer scope values, that are associated with the A-literals in centre chains. Scope values are initially set to 0, and might be modified when a reduction takes place. If the number of A-literals to the right of the A-literal involved is greater than its scope value, its scope value is set to that number of A-literals. On truncation of an A-literal, a lemma consisting of the negated A-literal and the negations of all A-literals whose scope values are equal to the numbers of A-literals to their right, is created. The scope values of the A-literals used is decremented. Lemma chains added to the input set can be used in subsequent extension operations. Using a lemma is equivalent to repeating (possibly an instance of) the subdeduction that lead to the creation of the lemma, i.e., the repetition is avoided.

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 chains Side clauses p(X) l(X) q + ~q l(Y) = p(X) l(X) [q]0 l(Y) + ~l(Z) ~m(S) r(Z) = p(X) l(X) [q]0 [l(Z)]0 ~m(S) r(Z) + ~r(b) ~l(T) ~s(b) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) ~s(b) + s(b) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) [~s(b)]0 + Truncate Lemma produced s(b) (Subsumed) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) + Reduce = p(X) l(X) [q]0 [l(b)]1 ~m(S) [r(b)]0 + Truncate Lemma produced ~l(b) ~r(b) = p(X) l(X) [q]0 [l(b)]0 ~m(S) + m(a) r(b) = p(X) l(X) [q]0 [l(b)]0 [~m(a)]0 r(b) + ~l(b) ~r(b) = p(X) l(X) [q]0 [l(b)]0 [~m(a)]0 [r(b)]0 ~l(b) + Reduce = p(X) l(X) [q]0 [l(b)]2 [~m(a)]0 [r(b)]0 + Truncate Lemma produced ~l(b) ~r(b) (Subsumed) = p(X) l(X) [q]0 [l(b)]1 [~m(a)]0 + Truncate Lemma produced ~l(b) m(a) (Subsumed later) = p(X) l(X) [q]0 [l(b)]0 + Truncate Lemma produced ~l(b) (Subsumes ~l(b) ~r(b), ~l(b) m(a)) = p(X) l(X) [q]0 + Truncate Lemma produced ~q (Subsumes ~q l(Y)) = p(X) l(X) + ~l(b) = p(b) [l(b)]0 + Truncate Lemma produced ~l(b) (Subsumed)) = p(b) + ~p(b) = [p(b)]0 + Truncate Lemma produced ~p(b) (Subsumed)) = FALSE

The steps that are repeated in the simple ME proof are only performed once here. The use of the lemma ~l(b) avoids the repeated subdeduction. The lemma 'contains' that subdeduction. The most striking feature of lemmas is their persistent nature - they remain in the input set even if the branch of the search which creates the lemma chain leads to failure. This has both beneficial and detrimental effects. On the up side, as in the example, a lemma chain can be used in a branch of the search other than that in which it was created. In the environment of a consecutively bounded search, a lemma created in one iteration of the search can be used in subsequent iterations. On the down side, the persistent nature of lemma chains often increases the size of the search space unacceptably, due to the increased number of side chains available for use in extension operations. This detrimental effect has been noted in various places, the principal problem being cited that "lemmas tend to be highly redundant - they are often subsumed by other lemmas and input chains" [Shostak, 1976, p. 63].

Practical Notes:

• As the lemma mechanism is not necessary for the completeness of the host deduction system, restrictions can be used to reduce this problem. Examples include keepig a lemma only if subsumes another clause, or additionally keeping unit lemmas. This approach has been taken by Fleisig, et al., [1974], whose implementation of the lemma mechanism includes a simplified subsumption test, and by Astrachan and Stickel [1992], whose METEOR system includes demodulation of lemmas and a subsumption test.

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

The Graph Construction (GC) Procedure

C-literals, introduced by the GC procedure, are inserted into the centre chain when an A-literal is truncated. C-literals act like lemmas under the constraint that if used any non-resolved upon literals can be A-reduced away. A C-literal is formed from the negation of the truncated A-literal. The point in the centre chain at which the C-literal is inserted is called the C-point of the truncated A-literal, and is immediately to the right of the rightmost A-literal that would be negated to form part of a lemma produced by the truncation, or at the leftmost end of the centre chain if there are no such A-literals. The scope values of the A-literals are decremented as if a lemma had been created. If a C-literal destined for the leftmost end is subsumed by an input clause then it is not inserted. B-literals may reduce against C-literals in a similar manner as against A-literals. The scope values of the A-literals whose scope values determined the insertion point of the C-literal are increased (to the number of A-literals to their right). C-reduction is equivalent to repeating (possibly an instance of) the subdeduction that lead to the insertion of the C-literal, i.e., the repetition is avoided.

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 chains Side clauses p(X) l(X) q + ~q l(Y) = p(X) l(X) [q]0 l(Y) + ~l(Z) ~m(S) r(Z) = p(X) l(X) [q]0 [l(Z)]0 ~m(S) r(Z) + ~r(b) ~l(T) ~s(b) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) ~s(b) + s(b) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) [~s(b)]0 + Truncate C-literal produced for left-most position s(b) (Subsumed and not inserted) = p(X) l(X) [q]0 [l(b)]0 ~m(S) [r(b)]0 ~l(T) + Reduce = p(X) l(X) [q]0 [l(b)]1 ~m(S) [r(b)]0 + Truncate C-literal produced {~r(b)} = p(X) l(X) [q]0 [l(b)]0 {~r(b)} ~m(S) + m(a) r(b) = p(X) l(X) [q]0 [l(b)]0 {~r(b)} [~m(a)]0 r(b) + C-reduce = p(X) l(X) [q]0 [l(b)]1 {~r(b)} [~m(a)]0 + Truncate C-literal produced {m(a)} = p(X) l(X) [q]0 [l(b)]0 {m(a)} {~r(b)} + Truncate C-literal produced {~l(b)} = {~l(b)} p(X) l(X) [q]0 + Truncate C-literal produced {~q} = {q} {~l(b)} p(X) l(X) + C-reduce = {q} {~l(b)} p(b) + ~p(b) = {q} {~l(b)} [p(b)]0 + Truncate C-literal produced {~p(b)} (Subsumed and not inserted) = {q} {~l(b)} + Truncate = FALSE

The steps that are repeated in the simple ME proof are only performed once here. The use of the C-literal {~l(b)} avoids the repeated subdeduction. The C-literal 'contains' that subdeduction.

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

Problem - limited choice of literal.