Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao zbMATH Openarrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
zbMATH Open
Article
Data sources: zbMATH Open
SIAM Journal on Computing
Article . 1988 . Peer-reviewed
Data sources: Crossref
DBLP
Article . 2018
Data sources: DBLP
versions View all 3 versions
addClaim

Existence, Uniqueness, and Construction of Rewrite Systems

Existence, uniqueness, and construction of rewrite systems
Authors: Nachum Dershowitz; Leo Marcus; Andrzej Tarlecki;

Existence, Uniqueness, and Construction of Rewrite Systems

Abstract

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.

Related Organizations
Keywords

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

  • BIP!
    Impact byBIP!
    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%
Powered by OpenAIRE graph
Found an issue? Give us feedback
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).
BIP!Citations provided by BIP!
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.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
19
Average
Top 10%
Top 10%
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!