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)}
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.
{(\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
![Math $I \models C \lor p$](/w/lib/exe/fetch.php?media=wiki:latex:/img662ec6ef8b89d3e0cab95969cdb40b46.png)
![Math $I \models D \lor \lnot p$](/w/lib/exe/fetch.php?media=wiki:latex:/imga47154e520bb921727ce86a3513ff21a.png)
![Math $I(p)={\it true}$](/w/lib/exe/fetch.php?media=wiki:latex:/imgcec6574b1e5ef7a40a42d7f9177504d0.png)
![Math $I \models D \lor \lnot p$](/w/lib/exe/fetch.php?media=wiki:latex:/imga47154e520bb921727ce86a3513ff21a.png)
![Math $I \models D$](/w/lib/exe/fetch.php?media=wiki:latex:/img2f2f98534692cc079175b91c5caf00ef.png)
![Math $I \models C\lor D$](/w/lib/exe/fetch.php?media=wiki:latex:/img4b5dc88cd44ac708e835cdb8fd4450ec.png)
![Math $I(p)={\it false}$](/w/lib/exe/fetch.php?media=wiki:latex:/img60195f9a9b4cd5422425ef51d1d977f8.png)
![Math $I \models C \lor p$](/w/lib/exe/fetch.php?media=wiki:latex:/img662ec6ef8b89d3e0cab95969cdb40b46.png)
![Math $I \models C$](/w/lib/exe/fetch.php?media=wiki:latex:/imge90a754c7861f054d3b91eb759a1c650.png)
![Math $I \models C\lor D$](/w/lib/exe/fetch.php?media=wiki:latex:/img4b5dc88cd44ac708e835cdb8fd4450ec.png)
![Math $C_1,C_2 \in S$](/w/lib/exe/fetch.php?media=wiki:latex:/imgb9499c7ebf99784b987f97c1d99aa9cd.png)
![Math $C_3$](/w/lib/exe/fetch.php?media=wiki:latex:/imgd19cc08043728c4034ea85a9fd4e254f.png)
![Math $C_1,C_2$](/w/lib/exe/fetch.php?media=wiki:latex:/img52480c8a8db9958406e6ab7faa50bb63.png)
![Math $I \models S$](/w/lib/exe/fetch.php?media=wiki:latex:/imga0e707aaf9ad2d510c389d7c975d0216.png)
![Math $I \models (S \cup \{ C_3 \})$](/w/lib/exe/fetch.php?media=wiki:latex:/imgdfb8f032a1576069934cabc7242fbb4a.png)