
doi: 10.1137/0217039
Based on the paper ``Existence and construction of rewrite systems'' by \textit{N. Dershowitz} and \textit{L. Marcus} [ATR-82(8478)-3, The Aerospace Corporation (1982)], this paper gives partial answers to the following questions: when does a given decidable equational theory have a decision procedure in the form of a canonical rewrite system, and when does the Knuth-Bendix procedure generate such a rewrite system for a given equational theory? More precisely, in the third section it is shown that there are decidable equational theories which require an expanded language in the order to obtain a canonical rewrite system to decide them, and others which do not have canonical rewrite systems in any language. The section four establishes conditions which imply the uniqueness of a term-rewriting system modulo a congruence and the section five considers the relationship between the Knuth-Bendix completion procedure and the existence of a finite canonical rewrite system for an equational theory.
termination, Mechanization of proofs and logical operations, Knuth-Bendix completion procedure, Equational logic, Mal'tsev conditions, Equational classes, universal algebra in model theory, equational theories, Abstract data types; algebraic specification, Theorem proving (deduction, resolution, etc.), term-rewriting system modulo a congruence
termination, Mechanization of proofs and logical operations, Knuth-Bendix completion procedure, Equational logic, Mal'tsev conditions, Equational classes, universal algebra in model theory, equational theories, Abstract data types; algebraic specification, Theorem proving (deduction, resolution, etc.), term-rewriting system modulo a congruence
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 19 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
