Existence, uniqueness, and construction of rewrite systems

The construction of term-rewriting systems, specifically by the Knuth-Bendix completion procedure, is considered. We look for conditions that might ensure the existence of a finite canonical rewriting system for a given equational theory and that might guarantee that the completion procedure will fi...

Full description

Saved in:
Bibliographic Details
Published in:SIAM journal on computing 1988-08, Vol.17 (4), p.629-639
Main Authors: DERSHOWITZ, N, MARCUS, L, TARLECKI, A
Format: Article
Language:English
Subjects:
Algebra
Applied sciences
Computer science
Computer science
control theory
systems
Exact sciences and technology
Language theory and syntactical analysis
Theoretical computing
Variables
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The construction of term-rewriting systems, specifically by the Knuth-Bendix completion procedure, is considered. We look for conditions that might ensure the existence of a finite canonical rewriting system for a given equational theory and that might guarantee that the completion procedure will find it. We define several notions of equivalence between rewriting systems in the ordinary and modulo case, and examine uniqueness of systems and the need for backtracking in implementing completion.
ISSN:0097-5397
1095-7111
DOI:10.1137/0217039