

Introduction to Logic

Tools for Thought


One of the disadvantages of using the resolution rule in an unconstrained manner is that it leads to many useless inferences. Some
inferences are redundant in that their conclusions can be derived in other ways. Some inferences are irrelevant in that they do not lead to derivations of the desired result.
This section presents a number of strategies for eliminating useless work. In reading this material, it is important to bear in mind that we are concerned here not with the order in which inferences are done, but only with the size of a resolution graph and with ways of decreasing that size by eliminating useless deductions.

Pure Literal Elimination
A literal occurring in a clause set is pure if and only if it has no instance that is complementary to an instance of another literal in the clause set. A clause that contains a pure literal is useless for the purposes of refutation, since the literal can never be resolved away. Consequently, we can safely remove such a clause. Removing clauses with pure literals defines a deletion strategy known as pureliteral elimination.
The clause set that follows is unsatisfiable. However, in proving this we can ignore the second and third clauses, since they both contain the pure literal s. The example in this case involves clauses in Propositional Logic, but it applies equally well to Relational Logic.
{¬p, ¬q, r} 
{¬p, s} 
{¬q, s} 
{p} 
{q} 
{¬r} 

Note that, if a database contains no pure literals, there is no way we can derive any clauses with pure literals using resolution. The upshot is that we do not need to apply the strategy to a database more than once, and in particular we do not have to check each clause as it is generated.

Tautology Elimination
A tautology is a clause containing a pair of complementary literals. For example, the clause {p(f(a)), ¬p(f(a))} is a tautology. The clause {p(x), q(y), ¬q(y ), r(z)} also is a tautology, even though it contains additional literals.
As it turns out, the presence of tautologies in a set of clauses has no effect on that set's satisfiability. A satisfiable set of clauses remains satisfiable, no matter what tautologies we add. An unsatisfiable set of clauses remains unsatisfiable, even if we remove all tautologies. Therefore, we can remove tautologies from a database, because we need never use them in subsequent inferences. The corresponding deletion strategy is called tautology elimination.

Note that the literals in a clause must be exact complements for tautology elimination to apply. We cannot remove nonidentical literals, just because they are complements under unification. For example, the clauses {¬p(a), p(x)}, {p(a)}, and {¬p(b)} are unsatisfiable. However, if we were to remove the first clause, the remaining clauses would be satisfiable.

Subsumption Elimination
In subsumption elimination, the deletion criterion depends on a relationship between two clauses in a database. A clause Φ subsumes a clause Ψ if and only if there exists a substitution σ such that Φσ ⊆ Ψ. For example, {p(x), q(y)} subsumes {p(a), q(v), r(w)}, since there is a substitution {x←a, y←v} that makes the former clause a subset of the latter.
If one member in a set of clauses subsumes another member, then the set remaining after eliminating the subsumed clause is satisfiable if and only if the original set is satisfiable. Therefore, subsumed clauses can be eliminated. Since the resolution process itself can produce tautologies and subsuming clauses, we need to check for tautologies and subsumptions as we perform resolutions.

Unit Resolution
A unit resolvent is one in which at least one of the parent clauses is a unit clause, i.e. one containing a single literal. A unit derivation is one in which all derived clauses are unit resolvents. A unit refutation is a unit derivation of the empty clause.

As an example of a unit refutation, consider the following proof. In the first two inferences, unit clauses from the initial set are resolved with binary clauses to produce two new unit clauses. These are resolved with the first clause to produce two additional unit clauses. The elements in these two sets of results are then resolved with each other to produce the contradiction. Note that our proof contains only a subset of the possible uses of the resolution rule. For example, clauses 1 and 2 can be resolved to derive the conclusion {q, r}, but this would not be a unit resolution.
1.  {p, q}  Premise 
2.  {¬p, r}  Premise 
3.  {¬q, r}  Premise 
4.  {¬r}  Premise 
5.  {¬p}  2, 4 
6.  {¬q}  3, 4 
7.  {q}  1, 5 
8.  {p}  1, 6 
9.  {r}  3, 7 
10.  {}  6, 7 

Inference procedures based on unit resolution are easy to implement and are usually quite efficient. It is worth noting that, whenever a clause is resolved with a unit clause, the conclusion has fewer literals than the parent does. This helps to focus the search toward producing the empty clause and thereby improves efficiency.
Unfortunately, inference procedures based on unit resolution generally are not complete. For example, the clauses {p, q}, {¬p, q}, {p ,¬q}, and {¬p, ¬q} are inconsistent. Using general resolution, it is easy to derive the empty clause. However, unit resolution fails in this case, since none of the initial clauses contains just one literal.
On the other hand, if we restrict our attention to Horn clauses (i.e. clauses with at most one positive literal), the situation is much better. In fact, it can be shown that there is a unit refutation of a set of Horn clauses if and only if it is unsatisfiable.

Input Resolution
An input resolvent is one in which at least one of the two parent clauses is a member of the initial (i.e., input) database. An input deduction is one in which all derived clauses are input resolvents. An input refutation is an input deduction of the empty clause.

It can be shown that unit resolution and input resolution are equivalent in inferential power in that there is a unit refutation from a set of sentences whenever there is an input refutation and vice versa.
One consequence of this fact is that input resolution is complete for Horn clauses but incomplete in general. The unsatisfiable set of clauses {p, q}, {¬p, q}, {p ,¬q}, and {¬p, ¬q} provides an example of a deduction on which input resolution fails. An input refutation must (in particular) have one of the parents of {} be a member of the initial database. However, to produce the empty clause in this case, we must resolve either two single literal clauses or two clauses having singleliteral factors. None of the members of the base set meet either of these criteria, so there cannot be an input refutation for this set.

Linear Resolution
Linear resolution (also called ancestryfiltered resolution) is a slight generalization of input resolution. A linear resolvent is one in which at least one of the parents is either in the initial database or is an ancestor of the other parent. A linear deduction is one in which each derived clause is a linear resolvent. A linear refutation is a linear deduction of the empty clause.
Linear resolution takes its name from the linear shape of the proofs it generates. A linear deduction starts with a clause in the initial database (called the top clause) and produces a linear chain of resolution. Each resolvent after the first one is obtained from the last resolvent (called the near parent) and some other clause (called the far parent). In linear resolution, the far parent must either be in the initial database or be an ancestor of the near parent.
Much of the redundancy in unconstrained resolution derives from the resolution of intermediate conclusions with other intermediate
conclusions. The advantage of linear resolution is that it avoids many useless inferences by focusing deduction at each point on the ancestors of each clause and on the elements of the initial database.

Linear resolution is known to be refutation complete. Furthermore, it is not necessary to try every clause in the initial database as top clause. It can be shown that, if a set of clauses Δ is satisfiable and Δ∪{Φ} is unsatisfiable, then there is a linear refutation with Φ as top clause. So, if we know that a particular set of clauses is consistent, we need not attempt refutations with the elements of that set as top clauses.
A merge is a resolvent that inherits a literal from each parent such that this literal is collapsed to a singleton by the most general unifier. The completeness of linear resolution is preserved even if the ancestors that are used are limited to merges. Note that, in this example, the first resolvent (i.e., clause {q}) is a merge.

Set of Support Resolution
If we examine resolution traces, we notice that many conclusions come from resolutions between clauses contained in a portion of the database that we know to be satisfiable. For example, in many cases, the set of premises is satisfiable, yet many of the conclusions are obtained by resolving premises with other premises rather than the negated conclusion As it turns out, we can eliminate these resolutions without affecting the refutation completeness of resolution.
A subset Γ of a set Δ is called a set of support for Δ if and only if ΔΓ is satisfiable. Given a set of clauses Δ with set of support Γ, a set of support resolvent is one in which at least one parent is selected from Γ or is a descendant of Γ. A set of support deduction is one in which each derived clause is a set of support resolvent. A set of support refutation is a set of support deduction of the empty clause.

The following derivation is a set of support refutation, with the singleton set {¬r} as the set of support. The clause {¬r} resolves with {¬p, r} and {¬q, r} to produce {¬p} and {¬q}. These then resolve with clause 1 to produce {q} and {p}, which resolve to produce the empty clause.
1.  {p, q}  Premise 
2.  {¬p, r}  Premise 
3.  {¬q, r}  Premise 
4.  {¬r}  Set of Support 
5.  {¬p}  2, 4 
6.  {¬q}  3, 4 
7.  {q}  1, 5 
8.  {}  7, 6 

Obviously, this strategy would be of little use if there were no easy way of selecting the set of support. Fortunately, there are several ways this can be done at negligible expense. For example, in situations where we are trying to prove conclusions from a consistent database, the natural choice is to use the clauses derived from the negated goal as the set of support. This set satisfies the definition as long as the database itself is truly satisfiable. With this choice of set of support, each resolution must have a connection to the overall goal, so the procedure can be viewed as working backward from the goal. This is especially useful for databases in which the number of conclusions possible by working forward is larger. Furthermore, the goaloriented character of such refutations often makes them more understandable than refutations using other strategies.

Use the arrow keys to navigate.
Press the escape key to toggle all / one.

