LARA

Differences

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

Link to this comparison view

sav08:definition_of_propositional_resolution [2009/05/14 10:38]
vkuncak 		sav08:definition_of_propositional_resolution [2015/04/21 17:30]
Line 1: Line 1:
-====== Definition of Propositional Resolution ====== 
  
-Recall: 
-  * **literal** is a propositional variable $p \in V$ or its negation $\lnot p$. 
-  * **clause** is a disjunction of literals 
- 
- 
-===== Clauses as Sets of Literals ===== 
- 
-The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas: 
-  * $\models (L_1 \lor (L_2 \lor L_3) \leftrightarrow (L_1 \lor L_2) \lor L_3)$ 
-  * $\models (L_1 \lor L_2 \leftrightarrow L_2 \lor L_1)$ 
-  * $\models (L \lor L \leftrightarrow L)$ 
-We therefore represent clauses as //sets of literals//​. ​ For example, we represent the clause $\lnot p_3 \lor p_1 \lor \lnot p_2 \lor p_1$ as the set $\{p_1,​\lnot p_2,\lnot p_3\}$. ​ We represent //false// as an empty clause and we do not represent //true//. 
- 
-===== Resolution Rule ===== 
- 
-Viewing clauses as sets, propositional resolution is the following rule: 
- 
-\[ 
-\frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} 
-     {C \cup D} 
-\] 
- 
-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 ===== 
- 
-Steps: 
-  - 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 for Propositional Logic]]) 
-  - Keep applying resolution rule until either 
-     - empty clause $\emptyset$ is derived 
-     - application of the resolution rule produces no new clauses 
- 
-[[Example of Using Propositional Resolution]] 
- 
-===== Soundness of Resolution Rule ===== 
- 
-Suppose that $I \models C \lor p$ and $I \models D \lor \lnot p$.  If $I(p)={\it true}$, then from $I \models D \lor \lnot p$ we conclude $I \models D$ and therefore $I \models C\lor D$. Similarly, if $I(p)={\it false}$, then from $I \models C \lor p$ we conclude $I \models C$ and therefore $I \models C\lor D$.  ​ 
- 
-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.