Differences
This shows you the differences between two versions of the page.
— |
sav08:completeness_of_resolution_for_fol [2008/04/01 18:18] (current) vkuncak created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Completeness of Resolution for FOL ====== | ||
+ | |||
+ | **Lemma:** Application of instantiation followed by resolution can be replaced by application of mgu-resolution followed by instantiation. | ||
+ | |||
+ | **Lemma:** If empty clause is derived using instantiation with resolution, and instantiation then it can also be obtained by using mgu-resolution. | ||
+ | |||
+ | **Theorem:** The [[Definition of Resolution for FOL|mgu-resolution]] is complete for checking whether a set of clauses is contradictory. | ||