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.

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.

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.

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.

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.

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.