Ground reducibility is EXPTIME-complete

DOI10.1016/S0890-5401(03)00134-2zbMATH Open1090.68047OpenAlexW2133563196MaRDI QIDQ1887142FDOQ1887142

Authors: Hubert Comon, Florent Jacquemard 

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

Recommendations

• The HOM problem is EXPTIME-complete
• Testing for the ground (co-)reducibility property in term-rewriting systems
• The HOM Problem is EXPTIME-Complete
• Algorithms and reductions for rewriting problems. II.
• Deciding regularity of the set of instances of a set of terms with regular constraints is EXPTIME-complete

zbMATH Keywords

Computational complexityTree automataRewriting systemsComputer theorem-proving

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Grammars and rewriting systems (68Q42)

Cites Work

• Title not available (Why is that?)
• On sufficient-completeness and related properties of term rewriting systems
• Automata for reduction properties solving
• Sufficient-completeness, ground-reducibility and their complexity
• Haskell overloading is DEXPTIME-complete
• Automatic proofs by induction in theories without constructors
• Semantic confluence tests and completion methods
• Encompassment properties and automata with constraints
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Pumping, cleaning and symbolic constraints solving
• Reductions in tree replacement systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (15)

• Emptiness and finiteness for tree automata with global reflexive disequality constraints
• A proof method for local sufficient completeness of term rewriting systems
• Unique Normalization for Shallow TRS
• Proving weak properties of rewriting
• Alternating two-way AC-tree automata
• Non-linear rewrite closure and weak normalization
• Automated Induction with Constrained Tree Automata
• Specification and proof in membership equational logic
• Induction = I-axiomatization + first-order consistency.
• The HOM Problem is EXPTIME-Complete
• Sufficient completeness verification for conditional and constrained TRS
• Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
• Test sets for the universal and existential closure of regular tree languages.
• The HOM problem is EXPTIME-complete
• QUIXO is EXPTIME-complete

This page was built for publication: Ground reducibility is EXPTIME-complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1887142)