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:deriving_propositional_resolution [2008/03/19 17:15]
tatjana
sav08:deriving_propositional_resolution [2012/05/01 12:26]
vkuncak
Line 44: Line 44:
    ​ProjectSet(S,​p) = \{ ProjectForm(F_1,​F_2,​p) \mid F_1,F_2 \in S \}    ​ProjectSet(S,​p) = \{ ProjectForm(F_1,​F_2,​p) \mid F_1,F_2 \in S \}
 \] \]
- 
  
 ==== Projection Proof Rules ==== ==== Projection Proof Rules ====
  
-Th justified the use of $ProjectForm(F_1,​F_2,​p)$ as an inference rule.  We write such rule:+Above we justified the use of $ProjectForm(F_1,​F_2,​p)$ as an inference rule.  We write such rule:
 \[ \[
 \frac{F_1 \; \ F_2} \frac{F_1 \; \ F_2}
Line 62: Line 61:
 {{\it false}} {{\it false}}
 \] \]
-where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula). ​ This rule is trivially sound. +where $F$ is formula that has no variables and that evaluates to //false// (ground contradictory formula). ​ This rule is trivially sound: we can never 
 +have a model of a ground formula that evaluates to false.
  
 ==== Iterating Rule Application ==== ==== Iterating Rule Application ====
Line 73: Line 72:
    ​P^*(S) = \bigcup_{n \geq 0} P_n(S)    ​P^*(S) = \bigcup_{n \geq 0} P_n(S)
 \end{array}\] \end{array}\]
- 
  
 ==== Completeness of Projection Rules ==== ==== Completeness of Projection Rules ====
Line 86: Line 84:
 The first statement follows from soundness of projection rules. ​ We next prove the second statement. The first statement follows from soundness of projection rules. ​ We next prove the second statement.
  
-Suppose that it ${\it false} \notin P^*(S)$. ​ We claim that $S$ is satisfiable. ​ We show that every finite set is satisfiable,​ so the property ​follows ​from the [[Compactness Theorem]].+Suppose that it ${\it false} \notin P^*(S)$. ​ We claim that $S$ is satisfiable. ​ We show that every finite set is satisfiable,​ so the property ​will follow ​from the [[Compactness Theorem]].
  
 Consider any finite $T \subseteq S$.  We show that $T$ it is satisfiable. ​ Let $T = \{F_1,​\ldots,​F_n\}$ and let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,​\ldots,​p_M\}$. ​ Consider the set Consider any finite $T \subseteq S$.  We show that $T$ it is satisfiable. ​ Let $T = \{F_1,​\ldots,​F_n\}$ and let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,​\ldots,​p_M\}$. ​ Consider the set
Line 137: Line 135:
  
 Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule. Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule.
 +