COMPLETNESS RESULTS FOR E-RESOLUTION

Abstract

Techniques are discussed for treating the equality relation within the framework of resolution based deductive systems for the first- order predicate calculus, utilized by researchers in the field of automatic theorem-proving by computer. E- resolution is defined as a restricted form of paramodulation and resolution, and proofs are given for the completeness of E-resolution and several modifications of E-resolution.