Virgil Emil CĂZĂNESCU, Denisa DIACONESCU
Completeness of Paramodulation without Lifting Lemma

Abstract. Equational logic programming deals with systems of equations in many-sorted algebras. Paramodulation is the main rule used for obtaining solutions. The lifting lemma is the most difficult step for proving the completeness. We prove without using a lifting lemma that every solution may be found using the paramodulation only.

READ THE PDF