Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:definition_of_propositional_resolution [2008/03/11 19:11] vkuncak |
sav08:definition_of_propositional_resolution [2009/05/14 10:38] vkuncak |
||
---|---|---|---|
Line 5: | Line 5: | ||
* **clause** is a disjunction of literals | * **clause** is a disjunction of literals | ||
- | ===== Clauses as Sets of Literlas ===== | + | |
+ | ===== Clauses as Sets of Literals ===== | ||
The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas: | The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas: | ||
Line 16: | Line 17: | ||
Viewing clauses as sets, propositional resolution is the following rule: | Viewing clauses as sets, propositional resolution is the following rule: | ||
+ | |||
\[ | \[ | ||
- | \frac{C \cup \{p\}\ \ \ D \cup \{\lnot p\}} | + | \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} |
{C \cup D} | {C \cup D} | ||
\] | \] | ||
- | where $C,D$ are clauses and $p \in V$ is a propositional variable. | + | |
+ | Here $C,D$ are clauses and $p \in V$ is a propositional variable. | ||
+ | |||
+ | Intuition: consider equivalent formulas | ||
+ | \[ | ||
+ | \frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)} | ||
+ | {(\lnot C) \rightarrow D} | ||
+ | \] | ||
+ | |||
+ | |||
===== Applying Resolution Rule to Check Satisfiability ===== | ===== Applying Resolution Rule to Check Satisfiability ===== | ||
Line 26: | Line 38: | ||
Steps: | Steps: | ||
- If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability. | - 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. | + | - Convert formula into polynomially large equisatisfiable formula in conjunctive normal form (see [[Normal Forms for Propositional Logic]]) |
- Keep applying resolution rule until either | - Keep applying resolution rule until either | ||
- empty clause $\emptyset$ is derived | - empty clause $\emptyset$ is derived | ||
- application of the resolution rule produces no new clauses | - application of the resolution rule produces no new clauses | ||
+ | [[Example of Using Propositional Resolution]] | ||
+ | |||
+ | ===== Soundness of Resolution Rule ===== | ||
+ | |||
+ | Suppose that $I \models C \lor p$ and $I \models D \lor \lnot p$. If $I(p)={\it true}$, then from $I \models D \lor \lnot p$ we conclude $I \models D$ and therefore $I \models C\lor D$. Similarly, if $I(p)={\it false}$, then from $I \models C \lor p$ we conclude $I \models C$ and therefore $I \models C\lor D$. | ||
+ | |||
+ | Therefore, if $C_1,C_2 \in S$ and $C_3$ is the result of applying resolution rule to $C_1,C_2$, then $I \models S$ if and only if $I \models (S \cup \{ C_3 \})$. Consequently, if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either. |