Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:deriving_propositional_resolution [2008/03/12 11:03] vkuncak |
sav08:deriving_propositional_resolution [2012/05/01 12:26] vkuncak |
||
|---|---|---|---|
| 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 ==== | ||
| - | 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 53: | Line 54: | ||
| \] | \] | ||
| 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 60: | 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 67: | Line 69: | ||
| \[\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}\] | ||
| - | |||
| ==== Completeness of Projection Rules ==== | ==== Completeness of Projection Rules ==== | ||
| Line 83: | 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 89: | Line 90: | ||
| A = \bigcup_{i=1}^M P_i(S) | A = \bigcup_{i=1}^M P_i(S) | ||
| \] | \] | ||
| - | By definition of $P_i$, we can show that the set $A$ contains the expansion of | + | By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of |
| \[ | \[ | ||
| \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n) | \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n) | ||
| \] | \] | ||
| - | This expansion is a ground formula, so it evaluates to either //true// or //false//. By assumption, $P^*(S)$ and therefore $A$ do not contain ground contradiction. Therefore, $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable. | + | Each of these conjuncts is a ground formula (all variables $p_1,\ldots,p_M$ have been instantiated), so the formula evaluates to either //true// or //false//. By assumption, $P^*(S)$ and therefore $A$ do not contain a ground contradiction. Therefore, each conjunct of $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable. |
| - | + | ||
| - | ==== Improvement: Simplification Rules ==== | + | |
| - | + | ||
| - | Of course, we do not need to wait until we reach a ground contradiction. Whenever we substitute variable with //true// or //false//, we can immediately simplify the formula using sound simplification rules. | + | |
| - | + | ||
| - | When we introduce simplifications we still manipulate equivalent formulas, so soundness and completeness remain the same. | + | |
| ==== Improvement: Subsumption Rules ==== | ==== Improvement: Subsumption Rules ==== | ||
| - | Note also that if $\models (F \rightarrow G)$, $F$ has been derived before, and $FV(G) \subseteq FV(F)$ then deriving $G$ does not help derive a ground contradiction, because the contradiction would also be derived using $F$. If we derive such formula, we can immediately delete it so that it does not slow us down. | + | Note also that if $\models (F \rightarrow G)$, where $F$ has been derived before, and $FV(G) \subseteq FV(F)$, then deriving $G$ does not help derive a ground contradiction, because the contradiction would also be derived using $F$. If we derive such formula, we can immediately delete it so that it does not slow us down. |
| In particular, a ground true formula can be deleted. | In particular, a ground true formula can be deleted. | ||