This is an old revision of the document!
Definition of Propositional Resolution
Recall:
- literal is a propositional variable or its negation .
- clause is a disjunction of literals
Clauses as Sets of Literals
The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas:
We therefore represent clauses as sets of literals. For example, we represent the clause as the set . We represent false as an empty clause and we do not represent true.
Resolution Rule
Viewing clauses as sets, propositional resolution is the following rule:
\[ \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}}
{C \cup D}
\]
Here are clauses and is a propositional variable.
1)
\lnot C) \rightarrow (\lnot p
2)
\lnot p) \rightarrow D)}
{(\lnot C) \rightarrow D}\] ===== Applying Resolution Rule to Check Satisfiability ===== Steps:
- If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability.
- Convert formula into polynomially large equisatisfiable formula in conjunctive normal form (see Normal Forms for Propositional Logic)
- Keep applying resolution rule until either
- empty clause is derived
- application of the resolution rule produces no new clauses
((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r))\] ===== Soundness of Resolution Rule ===== Suppose that and . If , then from we conclude and therefore . Similarly, if , then from we conclude and therefore . Therefore, if and is the result of applying resolution rule to , then if and only if . Consequently, if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either.