## 5.1 Introduction
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. ## 5.2 Clausal FormPropositional Resolution works only on expressions in A p¬p
A p¬ p¬p ∨ q
A p}{¬ p}{ ¬p, q}
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 (
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. ## 5.3 Resolution PrincipleThe idea of Propositional Resolution is simple. Suppose we have the clause { 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
The case we just discussed is an example. If we have the clause {
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 {
Resolving two singleton clauses leads to the
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
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 ( 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 (
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 (
## 5.4 Resolution ReasoningReasoning 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 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 In many cases, it is possible to find resolution derivations of conclusions from premises. Suppose, for example, we are given the clauses {¬
It is noteworthy that the resolution is not For example, given the clause { As another example, consider that valid clauses (such as { 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 {
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 As an example of a resolution proof, consider one of the problems we saw earlier. We have three premises -
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 ( 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. ## Recap
## ExercisesExercise 5.1: Convert the following sentences to clausal form.
Exercise 5.2: What are the results of applying Propositional Resolution to the following pairs of clauses.
Exercise 5.3: Use Propositional Resolution to show that the clauses { Exercise 5.4: Given the premises ( |