6.1 Introduction

Propositional Resolution is a powerful rule of inference for Propositional Logic. Using Propositional Resolution (without axiom schemata or other rules of inference), it is possible to build a theorem prover that is sound and complete for all of Propositional Logic. What's more, the search space using Propositional Resolution is much smaller than for standard Propositional Logic.

This chapter is devoted entirely to Propositional Resolution. We start with a look at clausal form, a variation of the language of Propositional Logic. We then examine the resolution rule itself. We close with some examples.

6.2 Clausal Form

Propositional Resolution works only on expressions in clausal form. Before the rule can be applied, the premises and conclusions must be converted to this form. Fortunately, as we shall see, there is a simple procedure for making this conversion.

A literal is either an atomic sentence or a negation of an atomic sentence. For example, if p is a logical constant, the following sentences are both literals.

A clausal sentence is either a literal or a disjunction of literals. If p and q are logical constants, then the following are clausal sentences.

A clause is the set of literals in a clausal sentence. For example, the following sets are the clauses corresponding to the clausal sentences above.

Note that the empty set {} is also a clause. It is equivalent to an empty disjunction and, therefore, is unsatisfiable. As we shall see, it is a particularly important special case.

As mentioned earlier, there is a simple procedure for converting an arbitrary set of Propositional Logic sentences to an equivalent set of clauses.The conversion rules are summarized below and should be applied in order.

1. Implications (I):

2. Negations (N):

3. Distribution (D):

4. Operators (O):

As an example, consider the job of converting the sentence (g ∧ (r ⇒ f)) to clausal form. The conversion process is shown below.

As a slightly more complicated case, consider the following conversion. We start with the same sentence except that, in this case, it is negated.

Note that, even though the sentences in these two examples are similar to start with (disagreeing on just one ¬ operator), the results are quite different.

6.3 Resolution Principle

The idea of Propositional Resolution is simple. Suppose we have the clause {p, q}. In other words, we know that p is true or q is true. Suppose we also have the clause {¬q, r}. In other words, we know that q is false or r is true. One clause contains q, and the other contains ¬q. If q is false, then by the first clause p must be true. If q is true, then, by the second clause, r must be true. Since q must be either true or false, then it must be the case that either p is true or r is true. So we should be able to derive the clause {p, r}.

This intuition is the basis for the rule of inference shown below. Given a clause containing a literal χ and another clause containing the literal ¬χ, we can infer the clause consisting of all the literals of both clauses without the complementary pair. This rule of inference is called Propositional Resolution or the Resolution Principle.

The case we just discussed is an example. If we have the clause {p, q} and we also have the clause {¬q, r}, then we can derive the clause {p, r} in a single step.

Note that, since clauses are sets, there cannot be two occurrences of any literal in a clause. Therefore, in drawing a conclusion from two clauses that share a literal, we merge the two occurrences into one, as in the following example.

If either of the clauses is a singleton set, we see that the number of literals in the result is less than the number of literals in the other clause. For example, from the clause {p, q, r} and the singleton clause {¬p}, we can derive the shorter clause {q, r}.

Resolving two singleton clauses leads to the empty clause; i.e. the clause consisting of no literals at all, as shown below. The derivation of the empty clause means that the database contains a contradiction.

If two clauses resolve, they may have more than one resolvent because there can be more than one way in which to choose the resolvents. Consider the following deductions.

Note, however, when two clauses have multiple pairs of complementary literals, only one pair of literals may be resolved at a time. For example, the following is not a legal application of Propositional Resolution.

If we were to allow this to go through, we would be saying that these two clauses are inconsistent. However, it is perfectly possible for (p ∨ q) to be true and (¬p ∨ ¬q) to be true at the same time. For example, we just let p be true and q be false, and we have satisfied both clauses.

It is noteworthy that resolution subsumes many of our other rules of inference. Consider, for example, Implication Elimination, shown below on the left. If we have (p ⇒ q) and we have p, then we can deduce q. The clausal form of the premises and conclusion are shown below on the right. The implication (p ⇒ q) corresponds to the clause {¬p, q}, and p corresponds to the singleton clause {p}. We have two clauses with a complementary literal, and so we cancel the complementary literals and derive the clause {q}, which is the clausal form of q.

As another example, recall the example of formal reasoning introduced in Chapter 1. We said that, whenever we have two rules in which the left hand side of one contains a proposition constant that occurs on the right hand side of the other, then we can cancel those constants and deduce a new rule by combining the remaining constants on the left hand sides of both rules and the remaining constants on the right hand sides of both rules. As it turns out, this is just Propositional Resolution.

Recall that we illustrated this rule with the deduction shown below on the left. Given (m ⇒ p ∨ q) and (p ⇒ q), we deduce (m ⇒ q). On the right, we have the clausal form of the sentences on the left. In place of the first sentence, we have the clause {¬m, p, q}; and, in place of the second sentence, we have {¬p, q}. Using resolution, we can deduce {¬m, q}, which is the clausal form of the sentence we derived on the left.

6.4 Resolution Reasoning

Reasoning with the Resolution Principle is analogous to reasoning with other rules of inference. We start with premises; we apply the Resolution Principle to those premises; we apply the rule to the results of those applications; and so forth until we get to our desired conclusion or we run out of things to do.

Formally, we define a resolution derivation of a conclusion from a set of premises to be a finite sequence of clauses terminating in the conclusion in which each clause is either a premise or the result of applying the Resolution Principle to earlier members of the sequence.

Note that our definition of resolution derivation is analogous to our definition of linear proof. However, in this case, we do not use the word proof, because we reserve that word for a slightly different concept, which is discussed below.

In many cases, it is possible to find resolution derivations of conclusions from premises. Suppose, for example, we are given the clauses {¬p, r} and {¬q, r} and {p, q}. Then we can derive the conclusion {r} as shown below.

It is noteworthy that the resolution is not generatively complete, i.e. it is not possible to find resolution derivations for all clauses that are logically entailed by a set of premise clauses.

For example, given the clause {p} and the clause {q}, there is no resolution derivation of {p, q}, despite the fact that it is logically entailed by the premises in this case.

As another example, consider that valid clauses (such as {p, ¬p}) are always true, and so they are logically entailed by any set of premises, including the empty set. However, Propositional Resolution requires some premises to have any effect. Given an empty set of premises, we would not be able to derive any conclusions, including these valid clauses.

On the other hand, we can be sure of one thing. If a set Δ of clauses is unsatisfiable, then there is guaranteed to be a resolution derivation of the empty clause from Δ. More generally, if a set Δ of Propositional Logic sentences is unsatisfiable, then there is guaranteed to be a resolution derivation of the empty clause from the clausal form of Δ.

As an example, consider the clauses {p, q}, {p, ¬q}, {¬p, q}, and {¬p, ¬q}. There is no truth assignment that satisfies all four of these clauses. Consequently, starting with these clauses, we should be able to derive the empty clause; and we can. A resolution derivation is shown below.

The good news is that we can use the relationship between unsatisfiability and logical entailment to produce a method for determining logical entailment as well. Recall that the Unsatisfiability Theorem introduced in Chapter 3 tells that a set Δ of sentences logically entails a sentence φ if and only if the set of sentences Δ∪{¬φ} is inconsistent. So, to determine logical entailment, all we need to do is to negate our goal, add it to our premises, and use Resolution to determine whether the resulting set is unsatisfiable.

Let's capture this idea with some definitions. A resolution proof of a sentence φ from a set Δ of sentences is a resolution derivation of the empty clause from the clausal form of Δ ∪ {¬φ}. A sentence φ is provable from a set of sentences Δ by Propositional Resolution (written Δ |- φ) if and only if there is a resolution proof of φ from Δ.

As an example of a resolution proof, consider one of the problems we saw earlier. We have three premises - p, (p ⇒ q), and (p ⇒ q) ⇒ (q ⇒ r). Our job is to prove r. A resolution proof is shown below. The first two clauses in the proof correspond to the first two premises of the problem. The third and fourth clauses in the proof correspond to the third premise. The fifth clause comes from the negation of the goal. Resolving the first clause with the second, we get the clause q, shown on line 6. Resolving this with the fourth clause gives us r. And resolving this with the clause on line 5 gives us the empty clause.

Here is another example, this time illustrating the way in which we can use Resolution to prove valid sentences. Let's say that we have no premises at all and we want to prove (p ⇒ (q ⇒ p)), an instance of the Implication Creation axiom schema.

The first step is to negate this sentence and convert to clausal form. A trace of the conversion process is shown below. Note that we end up with three clauses.

Finally, we take these clauses and produce a resolution derivation of the empty clause in one step.

One of the best features of Propositional Resolution is that it much more focussed than the other proof methods we have seen. There is no need to choose instantiations carefully or to search through infinitely many possible instantiations for rules of inference.

Moreover, unlike the other methods we have seen, Propositional Resolution can be used in a proof procedure that always terminates without losing completeness. Since there are only finitely many clauses that can be constructed from a finite set of proposition constants, the procedure eventually runs out of new conclusions to draw, and when this happens we can terminate our search for a proof.