Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:definition_of_propositional_resolution [2008/03/12 17:09] vkuncak |
sav08:definition_of_propositional_resolution [2009/05/14 10:39] 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 29: | Line 30: | ||
| {(\lnot C) \rightarrow D} | {(\lnot C) \rightarrow D} | ||
| \] | \] | ||
| + | |||
| + | |||
| + | |||
| ===== Applying Resolution Rule to Check Satisfiability ===== | ===== Applying Resolution Rule to Check Satisfiability ===== | ||
| Line 38: | Line 42: | ||
| - 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 | ||
| + | |||
| + | [[sav09:Example of Using Propositional Resolution]] | ||
| ===== Soundness of Resolution Rule ===== | ===== Soundness of Resolution Rule ===== | ||