On sufficient-completeness and related properties of term rewriting systems
type: Item
instance of: scholarly article
title: On sufficient-completeness and related properties of term rewriting systems
zbMATH Open document ID: 0594.68035
DOI: 10.1007/BF00292110
author: Deepak Kapur
author: Paliath Narendran
author: Hantao Zhang
published in: Acta Informatica
publication date: 1987-01-01T00:00:00Z
review text: The decidability of the sufficient-completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible with respect to the term rewriting system under consideration. These results are first shown for untyped systems and are subsequently extended to typed systems.
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3956433
zbMATH Keywords: decidability of the sufficient-completeness property of equational specifications
zbMATH Keywords: quasi-reducibility of a term
zbMATH Keywords: irreducible ground terms
zbMATH Keywords: normal forms
zbMATH Keywords: inductionless induction
MaRDI profile type: Publication
cites work: Confluent and Other Types of Thue Systems
cites work: Q3785921
cites work: Computing with rewrite systems
cites work: Q3880309
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Proofs by induction in equational theories with constructors
cites work: A finite Thue system with decidable word problem and without equivalent finite canonical system
cites work: Q5581665
cites work: Q3690200
cites work: Q3713575
cites work: Abstract Data Type Specification in the Affirm System
cites work: Complexity of certain decision problems about congruential languages
cites work: Q3956381
cites work: Some undecidability results for non-monadic Church-Rosser Thue systems
cites work: Semantic confluence tests and completion methods
Recommended article: Q3757892
Recommended article: Q3785921
Recommended article: Q4364373
Recommended article: On interreduction of semi-complete term rewriting systems
Recommended article: Q3347284
Recommended article: Completion for constrained term rewriting systems
Recommended article: Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems
Recommended article: A proof method for local sufficient completeness of term rewriting systems
Recommended article: Algebraic semantics and complexity of term rewriting systems
Recommended article: Q4376886
description: scientific article; zbMATH DE number 3956433