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 [2009/05/13 11:06] vkuncak |
sav08:definition_of_propositional_resolution [2009/05/14 10:00] vkuncak |
||
---|---|---|---|
Line 30: | Line 30: | ||
{(\lnot C) \rightarrow D} | {(\lnot C) \rightarrow D} | ||
\] | \] | ||
+ | |||
+ | |||
===== Applying Resolution Rule to Check Satisfiability ===== | ===== Applying Resolution Rule to Check Satisfiability ===== | ||
Line 40: | Line 42: | ||
- 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]]. | + | **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 ===== |