Rewrite method for theorem proving in first order theory with equality (Q1098649)

The purpose of this paper is the presentation of a complete rewrite rule method for predicate logic with equality, where unrestricted use of the equality predicate is allowed. A well known complete method for predicate logic, where equality may only appear in ``pure'' form (defining an equational theory), is narrowing combined with resolution [\textit{D. S. Lankford}, Canonical inference, Report ATP-32, Univ. Texas, Austin]; here paramodulation is already replaced by a Knuth-Bendix type method. The EN-strategy defined in this paper is an extension of the N-strategy developed by the author for the case of pure first order logic [Artif. Intell. 25, 225-300 (1985; Zbl 0558.68072)]; it is a pure completion method based on different critical pair concepts, the EN-, P-, merge- and para-critical pair (defined by the corresponding superposition concepts). In the reduction phase of the method, only N-rules (Boolean), P-rules and domain rules (for equality) are used to make the method more efficient. The power of the EN-strategy coincides with that of resolution combined with paramodulation; the advantage of the EN-strategy is the orientation of equalities into rules, while paramodulation is unoriented.