• English only

# Differences

This shows you the differences between two versions of the page.

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 =====