Lab for Automated Reasoning and Analysis LARA


This shows you the differences between two versions of the page.

Link to this comparison view

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.
sav08/completeness_of_resolution_for_fol.txt · Last modified: 2008/04/01 18:18 by vkuncak
© EPFL 2018 - Legal notice