
Introduction to Logic

Tools for Thought

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.
1.  {¬p, r}  Premise 
2.  {¬q, r}  Premise 
3.  {p, q}  Premise 
4.  {q, r}  1, 3 
5.  {r}  2, 4 

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.
1.  {p, q}  Premise 
2.  {p, ¬q}  Premise 
3.  {¬p, q}  Premise 
4.  {¬p, ¬q}  Premise 
5.  {p}  1, 2 
6.  {¬p}  3, 4 
7.  {}  5, 6 

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 Lesson 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.
1.  {p}  Premise 
2.  {¬p, q}  Premise 
3.  {p, ¬q, r}  Premise 
4.  {¬q, r}  Premise 
5.  {¬r}  Premise 
6.  {q}  1, 2 
7.  {r}  4, 6 
8.  {}  5, 7 

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.
 ¬(p ⇒ (q ⇒ p)) 
I  ¬(¬p ∨ (¬q ∨ p)) 
N  ¬¬p ∧ ¬(¬q ∨ p) 
 p ∧ (¬¬q ∧ ¬p) 
D  p ∧ q ∧ ¬p 
O  {p} 
 {q} 
 {¬p} 

Having done this, we take these clauses and produce a resolution derivation of the empty clause in one step.
1.  {p}  Premise 
2.  {q}  Premise 
3.  {¬p}  Premise 
4.  {}  1, 3 

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.

Use the arrow keys to navigate.
