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/12 11:03] vkuncak |
sav08:deriving_propositional_resolution [2008/03/12 11:04] vkuncak |
||
|---|---|---|---|
| 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. | ||
| - | |||