Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:deriving_propositional_resolution [2008/03/12 12:58] vkuncak |
sav08:deriving_propositional_resolution [2008/03/19 17:18] tatjana |
||
---|---|---|---|
Line 3: | Line 3: | ||
We next consider proof rules for checking [[Satisfiability of Sets of Formulas]]. | We next consider proof rules for checking [[Satisfiability of Sets of Formulas]]. | ||
- | We extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by | + | We are extending the notion of [[Substitution Theorems for Propositional Logic|substitution on formulas]] to sets of formulas by |
\[ | \[ | ||
subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} | subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} | ||
Line 12: | Line 12: | ||
We first derive a more abstract proof system and that show that resolution is a special case of it. | We first derive a more abstract proof system and that show that resolution is a special case of it. | ||
+ | |||
==== Key Idea ==== | ==== Key Idea ==== | ||
Line 41: | Line 42: | ||
Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by | Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by | ||
\[ | \[ | ||
- | Proj(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 ==== | ||
Line 53: | Line 55: | ||
\] | \] | ||
The soundness of projection rule follows from the fact that | The soundness of projection rule follows from the fact that | ||
- | for every interpretation $I$, if $I \models S$, then also $I \models Proj(S,p)$. | + | for every interpretation $I$, if $I \models S$, then also $I \models ProjectSet(S,p)$. |
Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the "ground contradiction rule" | Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the "ground contradiction rule" | ||
Line 61: | Line 63: | ||
\] | \] | ||
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. | ||
+ | |||
==== Iterating Rule Application ==== | ==== Iterating Rule Application ==== | ||
Line 67: | Line 70: | ||
\[\begin{array}{l} | \[\begin{array}{l} | ||
P_0(S) = S \\ | P_0(S) = S \\ | ||
- | P_{n+1}(S) = Proj(P_n(S),p_{n+1}) \\ | + | P_{n+1}(S) = ProjectSet(P_n(S),p_{n+1}) \\ |
P^*(S) = \bigcup_{n \geq 0} P_n(S) | P^*(S) = \bigcup_{n \geq 0} P_n(S) | ||
\end{array}\] | \end{array}\] | ||
+ | |||
Line 83: | 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 |