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/11 19:21]
vkuncak 		sav08:definition_of_propositional_resolution [2009/04/08 16:24]
philippe.suter
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 28: Line 35:
 Steps: Steps:
   - If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability.   - If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability.
-  - Convert formula into polynomially large equisatisfiable formula in conjunctive normal form (see [[Normal Forms of Propositional ​Formulas]])+  - Convert formula into polynomially large equisatisfiable formula in conjunctive normal form (see [[Normal Forms for Propositional ​Logic]])
   - Keep applying resolution rule until either   - Keep applying resolution rule until either
      - empty clause $\emptyset$ is derived      - empty clause $\emptyset$ is derived
Line 38: Line 45:
  
 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.
-