On sufficient-completeness and related properties of term rewriting systems
From MaRDI portal
Publication:1077161
DOI10.1007/BF00292110zbMath0594.68035MaRDI QIDQ1077161
Deepak Kapur, Han-Tao Zhang, Paliath Narendran
Publication date: 1987
Published in: Acta Informatica (Search for Journal in Brave)
normal formsinductionless inductiondecidability of the sufficient-completeness property of equational specificationsirreducible ground termsquasi-reducibility of a term
Related Items (42)
A proof method for local sufficient completeness of term rewriting systems ⋮ Computing linearizations using test sets ⋮ A proof system for conditional algebraic specifications ⋮ On sufficient completeness of conditional specifications ⋮ Design strategies for rewrite rules ⋮ Extending Bachmair's method for proof by consistency to the final algebra ⋮ Proving ground confluence and inductive validity in constructor based equational specifications ⋮ Ground reducibility is EXPTIME-complete ⋮ 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 ⋮ Proving Ramsey's theory by the cover set induction: A case and comparision study. ⋮ Sufficient-completeness, ground-reducibility and their complexity ⋮ Equality and disequality constraints on direct subterms in tree automata ⋮ Test sets for the universal and existential closure of regular tree languages. ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ Pumping, cleaning and symbolic constraints solving ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Undecidability of ground reducibility for word rewriting systems with variables ⋮ Narrowing based procedures for equational disunification ⋮ Testing for the ground (co-)reducibility property in term-rewriting systems ⋮ Decidability of regularity and related properties of ground normal form languages ⋮ Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications ⋮ Correctness of Context-Moving Transformations for Term Rewriting Systems ⋮ Proving weak properties of rewriting ⋮ Reachability analysis over term rewriting systems ⋮ Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness ⋮ On the connection between narrowing and proof by consistency ⋮ Applications and extensions of context-sensitive rewriting ⋮ Automating inductionless induction using test sets ⋮ Improving rewriting induction approach for proving ground confluence ⋮ Induction = I-axiomatization + first-order consistency.
Cites Work
- Proofs by induction in equational theories with constructors
- Some undecidability results for non-monadic Church-Rosser Thue systems
- A finite Thue system with decidable word problem and without equivalent finite canonical system
- Complexity of certain decision problems about congruential languages
- Computing with rewrite systems
- Semantic confluence tests and completion methods
- Abstract Data Type Specification in the Affirm System
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Confluent and Other Types of Thue Systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: On sufficient-completeness and related properties of term rewriting systems
