Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:definition_of_propositional_resolution [2009/05/14 10:39] vkuncak |
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*} |