Ground reducibility is EXPTIME-complete

DOI10.1016/S0890-5401(03)00134-2MaRDI QIDQ1887142zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4164137 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1414314 (Why is no real title available?)
• Automata for reduction properties solving
• Automatic proofs by induction in theories without constructors
• Encompassment properties and automata with constraints
• Haskell overloading is DEXPTIME-complete
• On sufficient-completeness and related properties of term rewriting systems
• Pumping, cleaning and symbolic constraints solving
• Reductions in tree replacement systems
• Semantic confluence tests and completion methods
• Sufficient-completeness, ground-reducibility and their complexity
• Testing for the ground (co-)reducibility property in term-rewriting systems

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)