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/12 17:08] vkuncak |
sav08:definition_of_propositional_resolution [2009/05/14 10:00] 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 24: | Line 25: | ||
Here $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 the form | + | Intuition: consider equivalent formulas |
\[ | \[ | ||
- | \frac{\lnot C \rightarrow \{\lnot p\}\ \ \ (\lnot p \rightarrow D)} | + | \frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)} |
- | {\lnot C \rightarrow D} | + | {(\lnot C) \rightarrow D} |
\] | \] | ||
+ | |||
+ | |||
===== Applying Resolution Rule to Check Satisfiability ===== | ===== Applying Resolution Rule to Check Satisfiability ===== | ||
Line 38: | Line 41: | ||
- 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:** prove a tautology from [[sav08:propositional_logic_informally|examples in this lecture]], e.g. | ||
+ | \[ | ||
+ | ((p \rightarrow q) \land\ ((\lnot p) \rightarrow r)) \leftrightarrow ((p \land q)\ \lor\ ((\lnot p) \land r)) | ||
+ | \] | ||
===== Soundness of Resolution Rule ===== | ===== Soundness of Resolution Rule ===== |