Rewrite method for theorem proving in first order theory with equality
type: Item
instance of: scholarly article
title: Rewrite method for theorem proving in first order theory with equality
zbMATH Open document ID: 0637.68104
DOI: 10.1016/S0747-7171(87)80024-X
author: Jieh Hsiang
published in: Journal of Symbolic Computation
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 4039346
zbMATH Keywords: rewrite rule
zbMATH Keywords: predicate logic with equality
zbMATH Keywords: EN-strategy
reviewed by: Alexander Leitsch
MaRDI profile type: Publication
cites work: Conditional rewrite rules: Confluence and termination
cites work: Proving Theorems with the Modification Method
cites work: Q5679729
cites work: Orderings for term-rewriting systems
cites work: Refutational theorem proving using term-rewriting systems
cites work: Q3703311
cites work: Q3674088
cites work: Q3786024
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3659124
cites work: Conditional rewrite rules
cites work: Q5581665
cites work: Equational methods in first order predicate calculus
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: Q5608782
Recommended article: Theorem proving with ordering and equality constrained clauses
Recommended article: Q3703311
Recommended article: Q3818295
Recommended article: Q3338214
Recommended article: Clausal rewriting
Recommended article: Equality, types, modules, and (why not?) generics for logic programming
Recommended article: Proof normalization for resolution and paramodulation
Recommended article: Theorem-proving with resolution and superposition
Recommended article: Completion for constrained term rewriting systems
description: scientific article; zbMATH DE number 4039346