Decidability and complexity of simultaneous rigid E-unification with one variable and related results

DOI10.1016/S0304-3975(98)00185-6zbMath0944.68103WikidataQ56765172 ScholiaQ56765172MaRDI QIDQ1575636

N. Delaunay

Publication date: 21 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

finite tree automata; logic with equality; rigid-unification

Mathematics Subject Classification ID

68Q45: Formal languages and automata

Related Items

TREE AUTOMATA BASED ON COMPLETE RESIDUATED LATTICE-VALUED LOGIC: REDUCTION ALGORITHM AND DECISION PROBLEMS, The undecidability of simultaneous rigid E-unification, Logic with equality: Partisan corroboration and shifted pairing, Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem, Monadic simultaneous rigid \(E\)-unification, Algebraic properties of complete residuated lattice valued tree automata, DKAL and Z3: A Logic Embedding Experiment

Cites Work

• The undecidability of simultaneous rigid E-unification
• Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
• Rigid E-unification: NP-completeness and applications to equational matings
• First-order modal tableaux
• Model theory.
• Bottom-up tree pushdown automata: Classification and connection with rewrite systems
• Haskell overloading is DEXPTIME-complete
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• Special cases and substitutes for rigid \(E\)-unification
• Tree acceptors and some of their applications
• Theorem Proving via General Matings
• Positive First-Order Logic Is NP-Complete
• An algorithm for reasoning about equality
• Lower Bounds on Herbrand's Theorem
• Theorem proving using equational matings and rigid E -unification
• Monadic simultaneous rigid E-unification and related problems
• Proof-search in intuitionistic logic based on constraint satisfaction
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
• Efficient ground completion
• Algebraic automata and context-free sets
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Mechanical Theorem-Proving by Model Elimination
• Tree generating regular systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item