Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:deriving_propositional_resolution [2008/03/19 17:15] tatjana |
sav08:deriving_propositional_resolution [2008/03/19 17:18] tatjana |
||
---|---|---|---|
Line 73: | Line 73: | ||
P^*(S) = \bigcup_{n \geq 0} P_n(S) | P^*(S) = \bigcup_{n \geq 0} P_n(S) | ||
\end{array}\] | \end{array}\] | ||
+ | |||
Line 86: | Line 87: | ||
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 |