In propositional logic, the procedure for producing a proof by resolution of proposition P with respect to a set of axioms F is the following.
ALGORITHM: PROPOSITIONAL RESOLUTION
1. Convert all the propositions of F to clause form
2. Negate P and convert the result to clause form. Add it to the set of clauses obtained in step 1.
3. Repeat until either a contradiction is found or no progress can be made:
a) Select two clauses. Call these the parent clauses.
b) Resolve them together. The resulting clause, called the resolvent, will be the disjunction of all of the literals of both of the parent clauses with the following exception: If there are any pairs of literals L and ¬L such that one of the parent clauses contains L and the other contains ¬L, then select one such pair and eliminate both L and ¬L from the resolvent.
c) If the resolvent is the empty clause, then a contradiction has been found. If it is not then add it to the set of clauses available to the procedure.
Suppose we are given the axioms shown in the first column of Table 1 and we want to prove R.First we convert the axioms to clause which is already in clause form. Then we begin selecting pairs of clauses to resolve together. Although any pair of clauses can be resolved, only those pairs that contain complementary literals will produce a resolvent that is likely to lead to the goal of sequence of resolvents shown in figure 1. We begin by resolving with the clause ⱷR since that is one of the clauses that must be involved in the contradiction we are trying to find.
One way of viewing the resolution process is that it takes a set of clauses that are all assumed to be true and based on information provided by the others, it generates new clauses that represent restrictions on the way each of those original clauses can be made true. A contradiction occurs when a clause becomes so restricted that there is no way it can be true. This is indicated by the generation of the empty clause.
| Sl. No | Given Axioms | Converted to Clause Form |
|---|---|---|
| 1 | P | P |
| 2 | (P˄Q) → R | ¬P˅Q˅R |
| 3 | (S˅T) → Q | ¬S˅Q |
| 4 | ¬T˅Q | |
| 5 | T | T |
Table 1: Some Facts in Propositional Logic
Figure 1: Resolution In Propositional Logic
In order for proposition 2 to be true, one of three things must be true: øP, øQ, or R.But we are assuming øR is true. Given that, the only way for proposition 2 to be true is for one of two things to be true: øP or øQ. That is what the first resolvent clause says. But proposition 1 says that P is true, which means that øP cannot be true, which leaves only one way for proposition 2 to be true, namely for øQ to be true. Proposition 4 can be true if either øT or Q is true. But since we now know that øQ must be true, the only way for proposition 4 to be true is for øT to be true. But proposition 5 says that T is true. Thus these clauses to be true in a single interpretation. This is indicated by the empty clause.