On sufficient-completeness and related properties of term rewriting systems
From MaRDI portal
(Redirected from Publication:1077161)
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.
Recommendations
- scientific article; zbMATH DE number 4006231
- scientific article; zbMATH DE number 4049024
- scientific article; zbMATH DE number 1088026
- On interreduction of semi-complete term rewriting systems
- scientific article; zbMATH DE number 3890721
- Completion for constrained term rewriting systems
- Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems
- A proof method for local sufficient completeness of term rewriting systems
- Algebraic semantics and complexity of term rewriting systems
- scientific article; zbMATH DE number 1118018
Cites work
- A finite Thue system with decidable word problem and without equivalent finite canonical system
- Abstract Data Type Specification in the Affirm System
- Complexity of certain decision problems about congruential languages
- Computing with rewrite systems
- Confluent and Other Types of Thue Systems
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- scientific article; zbMATH DE number 3913659 (Why is no real title available?)
- scientific article; zbMATH DE number 3943001 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 3776841 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Proofs by induction in equational theories with constructors
- Semantic confluence tests and completion methods
- Some undecidability results for non-monadic Church-Rosser Thue systems
Cited in
(65)- When is an extension of a specification consistent? Decidable and undecidable cases
- Narrowing based procedures for equational disunification
- Completion of rewrite systems with membership constraints. I: Deduction rules
- Extending Bachmair's method for proof by consistency to the final algebra
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- Test sets for the universal and existential closure of regular tree languages.
- On the descriptive power of term rewriting systems
- Induction = I-axiomatization + first-order consistency.
- Ground reducibility is EXPTIME-complete
- Applications and extensions of context-sensitive rewriting
- A proof method for local sufficient completeness of term rewriting systems
- Stability of termination and sufficient-completeness under pushouts via amalgamation
- Sufficient-completeness, ground-reducibility and their complexity
- scientific article; zbMATH DE number 3890721 (Why is no real title available?)
- Proving injectivity of functions via program inversion in term rewriting
- On context-free rewriting with a simple restriction and its computational completeness
- The \Pi^0_2 -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity)
- scientific article; zbMATH DE number 3943001 (Why is no real title available?)
- scientific article; zbMATH DE number 4006231 (Why is no real title available?)
- scientific article; zbMATH DE number 4011938 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 4092759 (Why is no real title available?)
- Sufficient completeness verification for conditional and constrained TRS
- scientific article; zbMATH DE number 1222418 (Why is no real title available?)
- scientific article; zbMATH DE number 1114350 (Why is no real title available?)
- Proving termination by dependency pairs and inductive theorem proving
- Pumping, cleaning and symbolic constraints solving
- Narrowing trees for syntactically deterministic conditional term rewriting systems
- Proving ground confluence and inductive validity in constructor based equational specifications
- Computing ground reducibility and inductively complete positions
- Inductive proofs by specification transformations
- Proofs in parameterized specifications
- Program transformation and rewriting
- On relationship between term rewriting systems and regular tree languages
- Open problems in rewriting
- Encompassment properties and automata with constraints
- More problems in rewriting
- Towards an efficient construction of test sets for deciding ground reducibility
- Problems in rewriting III
- Equality and disequality constraints on direct subterms in tree automata
- Improving rewriting induction approach for proving ground confluence
- New Undecidability Results for Properties of Term Rewrite Systems
- Completion of rewrite systems with membership constraints
- On the connection between narrowing and proof by consistency
- Proving weak properties of rewriting
- Reachability analysis over term rewriting systems
- Correctness of Context-Moving Transformations for Term Rewriting Systems
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- Decidability of regularity and related properties of ground normal form languages
- Computing linearizations using test sets
- A proof system for conditional algebraic specifications
- On sufficient completeness of conditional specifications
- Design strategies for rewrite rules
- On interreduction of semi-complete term rewriting systems
- Higher-order proof by consistency
- Using induction and rewriting to verify and complete parameterized specifications
- Approximately satisfied properties of systems and simple language homomorphisms
- Undecidability of ground reducibility for word rewriting systems with variables
- Difference of constrained patterns in logically constrained term rewrite systems
- Testing for the ground (co-)reducibility property in term-rewriting systems
- A verified algorithm for deciding pattern completeness
- A nominal approach to equational problems in languages with binders
- A verified algorithm for deciding pattern completeness with optimal asymptotic complexity
- Automating inductionless induction using test sets
- Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
This page was built for publication: On sufficient-completeness and related properties of term rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1077161)
