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/05/14 10:38] 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*} |
Line 43: | Line 43: | ||
- application of the resolution rule produces no new clauses | - application of the resolution rule produces no new clauses | ||
- | [[Example of Using Propositional Resolution]] | + | [[sav09:Example of Using Propositional Resolution]] |
===== Soundness of Resolution Rule ===== | ===== Soundness of Resolution Rule ===== |