General Purpose Restrictions

Pure Literal Deletion

If an input clause has a literal for which there is no complimentarily unifiable literal in the input set, then that literal can never be resolved upon. Such literals are said to be pure. Clauses in the input set containing pure literals can be discarded. By discarding such clauses, more pure literals may be created. The process continues until no pure literals remain. If all clauses are discarded then the input set was satisfiable.

Example 
S = { q(a,T),
      ~p(Y,Z) | q(Z,Y),
      ~s,
      r(X) | p(X,a),
      ~q(a,b) | s }

r(X) | p(X,a) is pure by r(X)
~p(Y,Z) | q(Z,Y) is pure by ~p(Y,Z)

Tautology Deletion

In the basic resolution procedure, and most refinements of the resolution procedure, it can be shown that tautologies cannot be part of a refutation. Thus tautologous clauses can be discarded. Tautology deletion is applied to the input set and to each resolvant inferred.

Example with contrived control 
S = { r(X) | p(X,a),
      ~p(a,Y) | ~r(Y),
      ~p(b,Y) | ~r(Y),
      ~r(b),
      r(a) }

r(X) | p(X,a) is the ChosenClause
+ ~p(a,Y) | ~r(Y) » r(a) | ~r(a) (tautology)
+ ~p(b,Y) | ~r(Y) » r(b) | ~r(a)
+ ~r(b) » p(b,a)
r(b) | ~r(a) is the ChosenClause
etc, etc

Subsumption

Subsumption prevents the use of clauses that contain information that is the same as, or more specific than, information in other clauses. For example, if it is known that "everyone tells the truth", there is no point is also knowing (storing the information) that "Geoff tells the truth". The earlier information subsumes the latter. In terms of clauses, subsumption checks if a (subsuming) clause can do everything that a (subsumed) clause could do. If that is the case, the subsumed clause can be discarded because the subsuming clause can be used instead.

Clause C| subsumes clause D| iff there is an instance C|θ of C| such that each literal of C|θ is a literal of D|.

Example
wise(geoff)
Subsumed by wise(X)
θ = {X/geoff}
taller(jim,geoff) | wise(geoff) | taller(X,brother_of(X))
Subsumed by wise(Y) | taller(jim,Z)
θ = {Y/geoff, Z/geoff}
taller(jim,geoff)
Subsumed by taller(X,geoff) | taller(jim,Y)
θ = {X/jim, Y/geoff}

Example - Which subsume which? 
~p(b,a) | ~p(c,a) | q(X,f(c))
q(Y,f(T)) | ~p(T,a)
~p(Z,a) | q(f,f(Z))

θ subsumption insists that, in addition to the above restriction, the subsuming clause must have no more literals than the subsumed clause. When using binary resolution and factoring, θ subsumption must be used to maintain refutation completeness.

Introspective subsumption occurs when a clause in a set of clauses is subsumed by another clause in the set, in which case the subsumed clause is discarded. Introspective subsumption may be done on the input set. Forward subsumption occurs when a when inferred clause is subsumed by an existing clause, in which case the inferred clause is discarded. Backward subsumption occurs when an existing clause is subsumed by an inferred clause, in which case the existing clause is discarded. When a new clause is inferred, forward subsumption is applied, and if the clause is not forward subsumed, backwards subsumption is applied.

Subsumption is a critical component of any ATP system. Beware: some refinements of the resolution procedure are not compatible with subsumption checking.

The ANL Algorithm with Restrictions 

Repetitively do pure literal deletion, tautology deletion, and introspective
subsumption to the Input clauses, until no simplification is possible
Let CanBeUsed = {}
Let ToBeUsed = Input clauses
While Refutation not found && ToBeUsed not empty
    Select the ChosenClause from ToBeUsed
    Move the ChosenClause to CanBeUsed
    Infer all possible clauses using the ChosenClause and other clauses from CanBeUsed.
    As each clause is inferred do
        If the inferred clause is a tautology or has a pure literal then
            Discard the inferred clause
        ElseIf the inferred clause is forward subsumed by any clause in ToBeUsed or CanBeUsed then
            Discard the inferred clause
        Else Discard any clauses in ToBeUsed or CanBeUsed that are backward subsumed by the inferred clause
            If any clauses are subsumed in the XXXBeUsed then
                Repetitively do pure literal deletion to the XXXBeUsed
            If the inferred clause subsumes the ChosenClause then
                Stop and discard all other inferred clauses from this iteration of the loop
            Add the inferred clause to ToBeUsed

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

~r(b) | r(b) is a tautology
~r(a) | ~q(a) is subsumed by ~r(a)
q(a) | ~t(X,c) is pure
t(Y,c) | r(a) is pure
~p(b) is the ChosenClause
~r(a) is the ChosenClause
~r(c) is the ChosenClause
~p(S) | p(b) is the ChosenClause
+ ~p(b) » ~p(S)
Backward subsumes ~p(S) | p(b) (ChosenClause)
~p(b)
~p(S) is the ChosenClause
p(b) | r(Y) | p(Y) is the ChosenClause
p(b) | r(Y) | p(Y) + ~r(a) » p(b) | p(a)
+ ~r(c) » p(b) | p(c)
+ ~p(S) » r(Y) | p(Y)
Backward subsumes p(b) | r(Y) | p(Y) (ChosenClause)
Discard others p(b) | p(a)
p(b) | p(c)
r(Y) | p(Y) is the ChosenClause
+ ~r(a) » p(a)
+ ~r(c) » p(c)
+ ~p(S) » r(Y)
Backward subsumes r(Y) | p(Y) (ChosenClause)
Discard others p(a)
p(c)
r(Y) is the ChosenClause
+ ~r(a) » FALSE

Example 
S10 = { p(X) | ~p(f(X))
        ~p(a)
        p(S) | q(S) | r(S)
        ~q(T) | p(a)
        ~r(T) | p(a) }

Exam Style Questions

  1. Show the execution of the ANL loop with all restrictions, using least symbol count as the selection strategy, to derive the empty clause from the following. Use pure literal deletion, tautology deletion, and subsumption. Write the subsuming clause next to the crossed out subsumed clause. 
    S = { ~m(b) | p(Y) | ~m(Y),
      ~p(a),
      ~p(a) | ~q(a),
      t(Y,c) | p(a),
      q(a) | ~t(X,c),
      m(b),
      m(S) | ~m(b),
      ~p(b) | p(b),
      ~p(c) } 

    S = { p(X) | ~p(f(X))
      ~p(a)
      p(S) | q(S) | r(S)
      ~q(T) | p(a)
      ~r(T) | p(a) }