LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
sav08:definition_of_propositional_resolution [2008/03/12 10:55]
vkuncak 		sav08:definition_of_propositional_resolution [2008/03/12 17:09]
vkuncak
Line 18: Line 18:
  
 \[ \[
-\frac{C \cup \{p\}\ \ \ D \cup \{\lnot p\}}+\frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}}
      {C \cup D}      {C \cup D}
 \] \]
  
 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
 +\[
 +\frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)}
 +     ​{(\lnot C) \rightarrow D}
 +\]
  
 ===== Applying Resolution Rule to Check Satisfiability ===== ===== Applying Resolution Rule to Check Satisfiability =====
Line 38: Line 44:
  
 Therefore, if $C_1,C_2 \in S$ and $C_3$ is the result of applying resolution rule to $C_1,C_2$, then $I \models S$ if and only if $I \models (S \cup \{ C_3 \})$.  Consequently,​ if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either. Therefore, if $C_1,C_2 \in S$ and $C_3$ is the result of applying resolution rule to $C_1,C_2$, then $I \models S$ if and only if $I \models (S \cup \{ C_3 \})$.  Consequently,​ if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either.
-