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 [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 28: Line 34:
 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 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.
-