Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:definition_of_propositional_resolution [2009/04/08 16:24] philippe.suter |
sav08:definition_of_propositional_resolution [2009/05/13 11:06] vkuncak |
||
---|---|---|---|
Line 39: | Line 39: | ||
- 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]]. | ||
===== Soundness of Resolution Rule ===== | ===== Soundness of Resolution Rule ===== |