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
sav08:definition_of_propositional_resolution [2008/03/12 10:55]
vkuncak 		sav08:definition_of_propositional_resolution [2009/05/14 10:39]
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
 +
 +[[sav09:​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.
-