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

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?

q(Y,f(T)) | ~p(T,a) ~p(b,a) | ~p(c,a) | q(X,f(c)) ~p(c,a) | q(V,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 and each inferred 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.

The use is ...

When a new clause is inferred, forward subsumption is applied.
If the new clause is not forward subsumed, backwards subsumption is applied.
If the new clause backwards subsumes the chosen clause parent, inferencing stops and all other inferred clauses are discarded.
Introspective subsumption applied to remaining new clauses.

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

Do tautology deletion, introspective subsumption, pure literal deletion
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.
    Do tautology deletion, introspective subsumption, and pure literal deletion  on the inferred clauses
    Do forward subsumption on the inferred clauses
    Do backward subsumption on the inferred clauses
    If an inferred clause subsumes the ChosenClause then
        Discard all other inferred clauses 
    Add the remaining inferred clauses 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) }

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

The DISCOUNT Loop

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 pure then Discard the inferred clause ElseIf the inferred clause is forward subsumed by any clause in CanBeUsed then Discard the inferred clause Else Add the resolvant to ToBeUsed

Exam Style Questions

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