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

From MaRDI portal
scientific article
Language Label Description Also known as
English
Rewrite method for theorem proving in first order theory with equality
scientific article

    Statements

    Rewrite method for theorem proving in first order theory with equality (English)
    0 references
    0 references
    1987
    0 references
    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.
    0 references
    rewrite rule
    0 references
    predicate logic with equality
    0 references
    EN-strategy
    0 references

    Identifiers