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 [2009/05/14 10:38]
vkuncak
Line 5: Line 5:
   * **clause** is a disjunction of literals   * **clause** is a disjunction of literals
  
-===== Clauses as Sets of Literlas ​=====+ 
 +===== Clauses as Sets of Literals ​=====
  
 The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas: The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas:
Line 18: Line 19:
  
 \[ \[
-\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 32: 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
 +
 +[[Example of Using Propositional Resolution]]
  
 ===== Soundness of Resolution Rule ===== ===== Soundness of Resolution Rule =====
Line 38: Line 50:
  
 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.
-