This shows you the differences between two versions of the page.
sav08:completeness_of_resolution_for_fol [2008/04/01 18:18] (current)
|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.|