Semantic Refinements

Model Resolution

Model resolution imposes the restriction that one parent of each full resolution must be FALSE in a given interpretation. For the ANL loop, TRUE input clauses are placed in CanBeUsed, and FALSE input clauses are placed in ToBeUsed. The interpretation should be chosen so as to minimize the number of FALSE clauses.

Example, using KBO ω for clause selection

S13 = { p(X) | ~q(X,Y) | ~s [9] TRUE q(X,b) | r(X) [8] FALSE ~r(a) | t(Z) [7] TRUE s [2] FALSE ~p(X) | ~s [5] TRUE ~t(X) | ~s } [5] TRUE I = { p(X) → FALSE, q(X) → FALSE, r(X) → FALSE, s(X) → FALSE, t(X) → FALSE } ω maps all predicates and function symbols to 2, and all variables to 1. p(X) | ~q(X,Y) | ~s to the CanBeUsed ~r(a) | t(Z) to the CanBeUsed ~p(X) | ~s to the CanBeUsed ~t(X) | ~s to the CanBeUsed s is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~q(X,Y) [7] TRUE Backward subsumes p(X) | ~q(X,Y) | ~s + ~p(X) | ~s » ~p(X) [3] TRUE Backward subsumes ~p(X) | ~s + ~t(X) | ~s » ~t(X) [3] TRUE Backward subsumes ~t(X) | ~s ~p(X) is the ChosenClause ~t(X) is the ChosenClause p(X) | ~q(X,Y) is the ChosenClause q(X,b) | r(X) is the ChosenClause + ~r(a) | t(Z) » q(a,b) | t(Z) [9] FALSE + p(X) | ~q(X,Y) » p(X) | r(X) [6] FALSE p(X) | r(X) is the ChosenClause + ~r(a) | t(Z) » p(a) | t(Z) [7] FALSE + ~p(X) » r(X) [3] FALSE STOP Backward subsumes p(X) | r(X) Sibling removed p(a) | t(Z) Backward subsumes q(X,b) | r(X) r(X) is the ChosenClause + ~r(a) | t(Z) » t(Z) [3] FALSE Backward subsumes ~r(a) | t(Z) t(Z) is the ChosenClause + ~t(X) » FALSE

Model resolution is a refutation complete strategy

Proof
To be filled in. Based on forcing the two clauses to 'be from' different branches of the failure tree.

• P₁ resolution is model resolution using the negative interpretation.
• N₁ resolution is model resolution using the positive interpretation.
• P_p resolution is model resolution using a predicate partition.
• A FALSE preference strategy selects a FALSE ChosenClause in preference to a TRUE one.

The Set of Support Strategy

The Set of Support (SoS) strategy places some of the input clauses into the Set of Support, and all resolvants are put in the SoS. Resolution of two clauses not in the SoS is prohibited, i.e., at least one parent clause must be in the SoS. The SoS strategy is a weakened form of model resolution. For completeness, the initial SoS must be chosen such that the non-SoS clauses have a model, i.e., are satisfiable. This specification ensures that one parent is not necessarily TRUE in the model of the non-SoS clauses. Model resolution can be viewed as repeated application of the SoS strategy after each inference step.

The ANL algorithm implements the SoS strategy directly, with the ToBeUsed set holding the SoS and the remaining input clauses placed into the CanBeUsed set. This prevent the generation of resolvants from two clauses not in the SoS.

The choice of SoS (while retaining refutation completeness) is determined by semantic considerations. Two possible choices of SoS are all the negative clauses (the non-SoS clauses have the positive interpretation as a model) or all the positive clauses (the non-SoS clauses have the negative interpretation as a model). The smaller the SoS the more effective the restriction.

Example
S4 = { ~p(a), p(X) | l(X) | q, ~q | l(a), ~l(a) | r, ~r | ~l(Z) } SoS = { p(X) | l(X) | q }

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

Model Resolution with Ordering

Model resolution is compatible with ordering on the FALSE parent. Full resolution is still used, and the atoms of the resolved upon literals must be the largest in their clauses, in the completed refutation.

Example, using KBO for everything

S13 = { p(X) | ~q(X,Y) | ~s [9] TRUE q(X,b) | r(X) [8] FALSE ~r(a) | t(Z) [7] TRUE s [2] FALSE ~p(X) | ~s [5] TRUE ~t(X) | ~s } [5] TRUE I = { p(X) → FALSE, q(X) → FALSE, r(X) → FALSE, s(X) → FALSE, t(X) → FALSE } ω maps all predicates and function symbols to 2, and all variables to 1. ρ is alphabetic p(X) | ~q(X,Y) | ~s to the CanBeUsed ~r(a) | t(Z) to the CanBeUsed ~p(X) | ~s to the CanBeUsed ~t(X) | ~s to the CanBeUsed s is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~q(X,Y) [7] TRUE Backward subsumes p(X) | ~q(X,Y) | ~s + ~p(X) | ~s » ~p(X) [3] TRUE Backward subsumes ~p(X) | ~s + ~t(X) | ~s » ~t(X) [3] TRUE Backward subsumes ~t(X) | ~s ~p(X) is the ChosenClause ~t(X) is the ChosenClause p(X) | ~q(X,Y) is the ChosenClause q(X,b) | r(X) is the ChosenClause + p(X) | ~q(X,Y) » p(X) | r(X) [6] FALSE p(X) | r(X) is the ChosenClause + ~p(X) » r(X) [3] FALSE STOP Backward subsumes p(X) | r(X) Backward subsumes q(X,b) | r(X) r(X) is the ChosenClause + ~r(a) | t(Z) » t(Z) [3] FALSE Backward subsumes ~r(a) | t(Z) t(Z) is the ChosenClause + ~t(X) » FALSE

Model resolution, with Ordering on the FALSE parent, is refutation complete.

Proof
To be filled in. Based on forcing the two clauses to 'be from' different branches of the failure tree. The one from the branch which is FALSE in I has to use its deepest literal. Then the clause from the true branch has a sibling literal, and the failure tree gets smaller after the resolution.

Semantic Resolution

Consider the proof tree from the model resolution refutation of S3, and any path from a FALSE leaf clause towards the root of the tree:

Example
I = { p(X) → TRUE, r(X) → TRUE, s(X) → TRUE, q(X) → FALSE} S3 = { ~p(X) | q(X) | r(X) | s(X), (TRUE) ~r(Y), (FALSE) ~s(a), (FALSE) ~s(b), (FALSE) ~q(a), (TRUE) ~q(b), (TRUE) p(a) | p(b) } (TRUE)

On such a path, it is necessary that at some stage a FALSE clause must be reached (at latest, the root of the tree). In the path indicated in the above tree, the first FALSE clause reached is ~p(a) | q(a). Starting again towards the root, again a FALSE clause must be reached, in this case at q(a). So, a model resolution proof can be broken down into chunks that end with the production of a FALSE resolvant. In the above proof tree the chunks are:

Unordered semantic resolution builds refutations by creating such chunks. The FALSE clauses used are called electrons, and the single TRUE clause the nucleus. The intermediate clauses are not kept, but are instead regenerated, e.g., ~p(X) | q(X) | s(X) has to be generated twice. If an intermediate clause is forward subsumed, then that option in the chunk is abandoned. If an intermediate clause backward subsumes an existing clause, then the intermediate clause can replace the existing clause. These intermediate subsumption checks are often omitted in implementations (but the play off is not well known). For the ANL loop, TRUE input clauses are placed in CanBeUsed, and FALSE input clauses are placed in ToBeUsed. The first electron of each chunk is the ChosenClause. The nucleus and other electrons are taken from CanBeUsed.

Example, using KBO ω for clause selection

S13 = { p(X) | ~q(X,Y) | ~s [9] TRUE q(X,b) | r(X) [8] FALSE ~r(a) | t(Z) [7] TRUE s [2] FALSE ~p(X) | ~s [5] TRUE ~t(X) | ~s } [5] TRUE I = { p(X) → FALSE, q(X) → FALSE, r(X) → FALSE, s(X) → FALSE, t(X) → FALSE } ω maps all predicates and function symbols to 2, and all variables to 1. p(X) | ~q(X,Y) | ~s to the CanBeUsed ~r(a) | t(Z) to the CanBeUsed ~p(X) | ~s to the CanBeUsed ~t(X) | ~s to the CanBeUsed s is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~q(X,Y) [7] TRUE Discard + ~p(X) | ~s » ~p(X) [3] TRUE Discard + ~t(X) | ~s » ~t(X) [3] TRUE Discard q(X,b) | r(X) is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~s | r(X) TRUE Intermediate Keep going + s » p(X) | r(X) [6] FALSE + ~r(a) | t(Z) » q(a,b) | t(Z) [9] FALSE p(X) | r(X) is the ChosenClause + ~r(a) | t(Z) » p(a) | t(Z) [7] FALSE + ~p(X) | ~s » r(X) | ~s TRUE Intermediate Keep going + s » r(X) [3] FALSE STOP Backward subsumes p(X) | r(X) Sibling removed p(a) | t(Z) Backward subsumes q(X,b) | r(X) r(X) is the ChosenClause + ~r(a) | t(Z) » t(Z) [3] FALSE Backward subsumes ~r(a) | t(Z) Backward subsumes q(a,b) | t(Z) t(Z) is the ChosenClause + ~t(X) | ~s » ~s [2] TRUE Intermediate + s » FALSE

Example
I = { l(X) → FALSE, p(X) → FALSE, q → TRUE, r → TRUE } S4 = { ~p(a), (TRUE) p(X) | l(X) | q, (TRUE) ~q | l(a), (FALSE) ~l(a) | r, (TRUE) ~r | ~l(Z) } (TRUE)

Ordered Semantic Resolution

• The E_i are the electrons (satellites)
• N is the nucleus
• The E_i are FALSE in I
• Let R₁ = N. For each i=1..q, there is a (full) resolvant R_i+1 of R_i and E_i
• The resolved upon literals in E_i are the largest in E_i.
• R_q+1 is FALSE in I.

R_q+1 is called a PI-resolvant. A semantic resolution refutation is built from semantic clashes. A full resolvant is necessary (consider S = {p(X) | p(Y), ~p(X) | ~p(Y), I = {p(X) → FALSE}).

Example, using KBO for everything

S13 = { p(X) | ~q(X,Y) | ~s [9] TRUE q(X,b) | r(X) [8] FALSE ~r(a) | t(Z) [7] TRUE s [2] FALSE ~p(X) | ~s [5] TRUE ~t(X) | ~s } [5] TRUE I = { p(X) → FALSE, q(X) → FALSE, r(X) → FALSE, s(X) → FALSE, t(X) → FALSE } ω maps all predicates and function symbols to 2, and all variables to 1. ρ is alphabetic p(X) | ~q(X,Y) | ~s to the CanBeUsed ~r(a) | t(Z) to the CanBeUsed ~p(X) | ~s to the CanBeUsed ~t(X) | ~s to the CanBeUsed s is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~q(X,Y) [7] TRUE Discard + ~p(X) | ~s » ~p(X) [3] TRUE Discard + ~t(X) | ~s » ~t(X) [3] TRUE Discard q(X,b) | r(X) is the ChosenClause + p(X) | ~q(X,Y) | ~s » p(X) | ~s | r(X) TRUE Intermediate Keep going + s » p(X) | r(X) [6] FALSE p(X) | r(X) is the ChosenClause + ~p(X) | ~s » r(X) | ~s TRUE Intermediate Keep going + s » r(X) [3] FALSE STOP Backward subsumes p(X) | r(X) Backward subsumes q(X,b) | r(X) r(X) is the ChosenClause + ~r(a) | t(Z) » t(Z) [3] FALSE Backward subsumes ~r(a) | t(Z) t(Z) is the ChosenClause + ~t(X) | ~s » ~s [2] TRUE Intermediate + s » FALSE

Example
I = { l(X) → FALSE, p(X) → FALSE, q → TRUE, r → TRUE } S4 = { ~p(a), (TRUE) p(X) | l(X) | q, (TRUE) ~q | l(a), (FALSE) ~l(a) | r, (TRUE) ~r | ~l(Z) } (TRUE) O = l/1 > p/1 > q/0 > r/0

Ordered semantic resolution is refutation complete.

Proof
To be filled in. [Slagle 1967]

If binary resolution is used in semantic resolution, it is sufficient to factor only the electrons. This is possible because electrons can be reused to remove factorable literals in nuclei, and the duplicate literals in the resolvants factor away themselves. The initial electrons must be factored, and the resolvants are factored as they are created. This is the normal way of implementing semantic resolution and its specialisations. For the ANL loop, place all TRUE clauses in CanBeUsed, and FALSE clauses and FALSE factors in ToBeUsed.

Example
I = { p(X) → FALSE, q(X,Y) → FALSE, r(X,Y) → FALSE, s → FALSE, t(X) → FALSE} S5 = { p(X) | p(Y) | ~q(X,Y) | ~s, (TRUE) q(X,Y) | r(X,Y), (FALSE) ~r(a,b) | t(Y) | t(X), (TRUE) s, (FALSE) ~p(X), (TRUE) ~t(X) | ~t(Y) } (TRUE) O = p(X) > q(X,Y) > r(X,Y) > s > t(X)

Note that for positive, negative, and predicate-partition interpretations, factoring preserves FALSEness, so factored electrons remain electrons. For general interpretations this is not the case.

Example
I = { p(a) → FALSE, p(b) → TRUE, q(X) → FALSE } S = { p(X) | q(b) | q(X) } (FALSE) p(X) | q(b) | q(X) + Factoring » p(b) | q(b) (TRUE)

Hyper-resolution

Positive hyper-resolution is semantic resolution using the negative interpretation. Negative hyper-resolution is semantic resolution using the positive interpretation. AM-clash resolution is semantic resolution using a predicate partition.

Exam Style Questions

1. Show the execution of the ANL loop implementing model resolution, ordered model resolution, semantic resolution, and ordered semantic resolution, to derive the empty clause from the following. Use subsumption, writing the subsuming clause next to the crossed out subsumed clause. For ordering, use alphabetic predicate ordering, and then use KBO with ρ being alphabetic and ω mapping predicates to 3, functions to 2, and veriables to 1. For interpretation, use the positive interpretation, then the negative interpretation, and then a predicate partition with p and q mapping to TRUE and all other predicates to FALSE.

   S = { ~p(X) | q(X) | r(X)
         ~r(b)
         ~r(a)
         p(a) | p(b)
         ~q(Y) } 

   With four calculi, two orderings, and three interpretations, that's 18 derivations!