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.

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(d,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.

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.

Inference Rules

For problems without equality, the ANL algorithm is complete with binary resolution and binary factoring. Full resolvants are produced as follows:

Full factors are produced by repeatedly using binary factoring, placing the binary factors in the ToBeUsed, and when they are selected binary factoring again.
Full resolvants are produced by doing full factoring and then binary resolution.

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

The DISCOUNT loop is an alternative flexible algorithm for controlling the generation of inferred clauses. The DISCOUNT loop delays simplifications.

Let CanBeUsed = {}
Let ToBeUsed = Input clauses
While Refutation not found && ToBeUsed not empty
    Select the ChosenClause from ToBeUsed
    if (ChosenClause is not subsumed by a member of ToBeUsed or CanBeUsed)
        Remove all members of CanBeUsed subsumed by the ChosenClause
        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 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) } 
```