Semantic Resolution: a simple example

¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inferences Timestep 2 11 clauses 11 inferences Timestep 3 12 clauses 19 inferences Goal reached at step 3

The figure to the left shows the resolution graph for the toy problem of computing the closure under binary resolution of the clause set

p(x) | q(x)
¬p(x)
¬q(a) | ¬q(b)

Obviously, there are derivations of the empty clause from this set in just three steps of binary resolution, so the problem of showing it unsatisfiable is trivial. Here we consider not only the search for the first proof, but the computation of the entire space of reachable clauses (12 of them, in fact) saturated under resolution. Only 19 resolution inferences exist between the 12 reachable clauses, so the graph is not large, but it is enough to illustrate many of the phenomena which emerge when resolution is semantically constrained.

In the diagram of the graph, each black dot represents a binary resolution inference. The heavy blue edge connects it to the resolvent, and the two lighter edges to the two parent clauses. Subsumed clauses are shown in the diagram, although most theorem provers will delete them and draw no consequences from them. Some clauses, such as p(a), may be derived in more than one way; in such cases, all inferences with the clause as resolvent are retained in the graph.

As defined by Slagle (1967), semantic resolution might more appropriately be called semantic hyper-resolution. It makes use of an interpretation of the language called the guiding model. The inputs to the inference are one clause called the nucleus and an arbitrary number of other clauses (not necessarily all different) called satellites. The clash matches a literal in each satellite with a complementary literal in the nucleus; no literal in the nucleus is matched with more than one satellite literal. The hyper-resolvent consists of all literals which do not take part in the clash, after the unifying substitution is applied. Factoring to remove subsumed literals is built into the rule; additional factoring may be applied as a separate rule, though we do not presuppose this. The semantic constraint is that all satellites and the hyper-resolvent must be false in the guiding model. Here we also require that the nucleus be one of the input clauses (so no new nuclei are ever derived) though this restriction could be relaxed. For the purposes of these diagrams, we include hyper-resolvents which are true in the guiding model, even though such clauses may be dead-ends as they are not input clauses (so cannot be nuclei) and can never function as satellites.

We emulate semantic hyper-resolution using binary resolution, picking off the literals of the nucleus one by one. Since this results in intermediate clauses which are neither nuclei nor satellites, the inference must be re-defined for them. We treat them as nuclei, but restrict their clashable literals to be those inherited from their nucleus parent—i.e. the ones from the original nucleus which have not been clashed away yet.

The graph of semantic resolution as we have implemented it is therefore also a binary resolution graph. Some of the inferences will be missing, as they will be blocked by the semantic constraint on satellites or by the unavailability of literals for clashing. The graphs below show the effect of semantic resolution on this particular clause set, with different choices of guiding model.

¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inferences Timestep 2 11 clauses 10 inferences Timestep 3 12 clauses 18 inferences Goal reached at step 3 ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inferences Timestep 2 8 clauses 9 inferences Timestep 3 11 clauses 11 inferences Goal reached at step 3 Timestep 4 11 clauses 13 inferences

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = ∅, and I(q) = {a}.

This semantic constraint has virtually no effect. Only one of the 19 inferences is blocked, and all 12 clauses remain reachable in the same number of steps as before.

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a,b}, and also I(q) = {a,b}. Resolution constrained by the interpretation on which all atoms are true is known as negative hyperresolution.

The formula p(a) | p(b) is no longer reachable, and the unit clauses ¬p(a) and ¬p(b) are delayed, making some of the derivations of the empty clause longer than they were without the semantic constraint. Overall, the number of inferences required to exhaust the search space is reduced by about a third.

¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inferences Timestep 2 11 clauses 9 inferences Timestep 3 12 clauses 17 inferences Goal reached at step 3 ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) q(x) ¬q(a) ¬q(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 4 clauses 1 inference Timestep 2 6 clauses 3 inferences Timestep 3 7 clauses 5 inferences Goal reached at step 3

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = ∅, and also I(q) = ∅. Resolution constrained by the interpretation on which all atoms are false is known as (positive) hyperresolution.

Only two resolution inferences are blocked by this semantic constraint, and they would result in subsumed clauses in any case, so there is little effect on the unconstrained proof search.

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a,b}, and I(q) = ∅.

This shows semantic resolution working as intended. 5 of the 12 clauses derivable from the inputs using ordinary resolution are unreachable with this semantic restriction, reducing the search space almost to triviality and directing the proof search straight to the goal. Moreover, the proofs remaining in this reduced space are the shortest possible by binary resolution, so nothing is lost in terms of proof length.

¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 5 clauses 2 inferences Timestep 2 8 clauses 6 inferences Timestep 3 10 clauses 10 inferences Timestep 4 11 clauses 12 inferences Goal reached at step 4 ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inference Timestep 2 11 clauses 10 inferences Timestep 3 12 clauses 18 inferences Goal reached at step 3

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = ∅, and I(q) = {a,b}.

This graph shows neatly why semantic resolution is good and bad. Only one clause becomes unreachable, but as it is heavily used, this reduces the number of inferences by around a third. The search space is thus reduced and the proof search focussed more closely on the eventual proofs than it was without semantic constraint. However, the deleted clause occurs in all of the shortest proofs, so the search must continue for an extra level before proofs are found, and they are longer than before.

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a}, and also I(q) = {a}.

The effect of this semantic constraint is negligible. Although 5 of the 12 clauses are true in the guiding model, only one inference is blocked, and there is no significant change to the proof search.

¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(a) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 4 clauses 1 inference Timestep 2 6 clauses 3 inferences Timestep 3 8 clauses 6 inferences Goal reached at step 3 Timestep 4 8 clauses 7 inferences ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inference Timestep 2 11 clauses 10 inferences Timestep 3 12 clauses 17 inferences Goal reached at step 3

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a,b}, and I(q) = {a}.

Semantic resolution with this model is quite effective at reducing the search space. 4 of the 12 clauses are not reachable, so there is a reduction in the number of inferences from 19 to 7. Two of the 3-step proofs remain, but the others are blocked. There is also an irredundant 4-step proof which was previously subsumed.

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a}, and I(q) = {a,b}.

The semantic resolution constraint with this model blocks just 2 of the 19 binary resolution inferences, and all 12 of the clauses remain reachable in largely the same way as they are without the semantic restriction. Hence the overall effect is very small.

\ ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 4 clauses 1 inference Timestep 2 6 clauses 3 inferences Timestep 3 8 clauses 6 inferences Goal reached at step 3 Timestep 4 8 clauses 7 inferences ¬p(x) p(x) | q(x) ¬q(a) | ¬q(b) p(b) | ¬q(a) p(a) | ¬q(b) q(x) ¬q(a) ¬q(b) p(b) p(a) p(a) | p(b) ⊥ Timestep 0 3 clauses 0 inferences Goal not reached Timestep 1 6 clauses 3 inferences Timestep 2 11 clauses 9 inferences Timestep 3 12 clauses 14 inferences Goal reached at step 3

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a}, and I(q) = {b}.

The effect of using this model is exactly like that seen in the graph above, except for reversing the roles of a and b.

Semantic resolution graph for the clause set {p(x) | q(x), ¬p(x), ¬q(a) | ¬q(b)}. The guiding model has I(p) = {a}, and I(q) = ∅.

This semantic constraint has some effect: 5 of the 19 inferences are blocked. All 12 formulae remain reachable, but one of them (p(a) | p(b)) is useless, as it is true and unavailable as a nucleus, so it will be deleted in fact.