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 [2009/04/08 16:24] philippe.suter |
sav08:definition_of_propositional_resolution [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 18: | Line 18: | ||
| Viewing clauses as sets, propositional resolution is the following rule: | Viewing clauses as sets, propositional resolution is the following rule: | ||
| - | \[ | + | \begin{equation*} |
| \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} | \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} | ||
| {C \cup D} | {C \cup D} | ||
| - | \] | + | \end{equation*} |
| 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 equivalent formulas | Intuition: consider equivalent formulas | ||
| - | \[ | + | \begin{equation*} |
| \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} | ||
| - | \] | + | \end{equation*} |
| + | |||
| + | |||
| ===== Applying Resolution Rule to Check Satisfiability ===== | ===== Applying Resolution Rule to Check Satisfiability ===== | ||
| Line 39: | 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 ===== | ||