Lab for Automated Reasoning and Analysis LARA

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