Ground reducibility is EXPTIME-complete
From MaRDI portal
Publication:1887142
DOI10.1016/S0890-5401(03)00134-2zbMath1090.68047OpenAlexW2133563196MaRDI QIDQ1887142
Florent Jacquemard, Hubert Comon
Publication date: 23 November 2004
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00134-2
Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items
A proof method for local sufficient completeness of term rewriting systems, Alternating two-way AC-tree automata, Test sets for the universal and existential closure of regular tree languages., Sufficient completeness verification for conditional and constrained TRS, Automated Induction with Constrained Tree Automata, Specification and proof in membership equational logic, Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications, Proving weak properties of rewriting, The HOM Problem is EXPTIME-Complete, Unique Normalization for Shallow TRS, Induction = I-axiomatization + first-order consistency., Non-linear rewrite closure and weak normalization, Emptiness and finiteness for tree automata with global reflexive disequality constraints
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Testing for the ground (co-)reducibility property in term-rewriting systems
- On sufficient-completeness and related properties of term rewriting systems
- Reductions in tree replacement systems
- Haskell overloading is DEXPTIME-complete
- Automatic proofs by induction in theories without constructors
- Automata for reduction properties solving
- Sufficient-completeness, ground-reducibility and their complexity
- Semantic confluence tests and completion methods
- Pumping, cleaning and symbolic constraints solving
- Encompassment properties and automata with constraints
