Example | ||||||
---|---|---|---|---|---|---|
S = { q(a,T), ~p(Y,Z) | q(Z,Y), ~s, r(X) | p(X,a), ~q(a,b) | s }
|
Example with contrived control | ||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S = { r(X) | p(X,a), ~p(a,Y) | ~r(Y), ~p(b,Y) | ~r(Y), ~r(b), r(a) }
|
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 | |||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
Example - Which subsume which? |
---|
|
θ 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.
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) } }
|
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 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
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) }