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 Lesson 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.