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 11:02] vkuncak |
sav08:deriving_propositional_resolution [2008/03/12 11:04] vkuncak |
||
|---|---|---|---|
| Line 89: | Line 89: | ||
| 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 each conjunct of the conjunctive normal form of the expansion of | + | By definition of $P_i$, we can show that the set $A$ contains 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) | ||
| \] | \] | ||
| - | All these conjuncts are ground, so they evaluate to either //true// or //false//. By assumption, $P^*(S)$ and therefore $A$ do not contain ground contradiction. Therefore, all these conjuncts are true, so $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable. | + | 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. |
| ==== Improvement: Simplification Rules ==== | ==== Improvement: Simplification Rules ==== | ||
| Line 103: | Line 103: | ||
| ==== 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. | ||
| Line 140: | Line 140: | ||
| 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. | ||
| - | |||