LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:deriving_propositional_resolution [2008/03/19 17:18]
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 138: 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.
 +