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. | ||
- |