Decidability and complexity of simultaneous rigid E-unification with one variable and related results
From MaRDI portal
Publication:1575636
DOI10.1016/S0304-3975(98)00185-6zbMath0944.68103WikidataQ56765172 ScholiaQ56765172MaRDI QIDQ1575636
Publication date: 21 August 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
68Q45: Formal languages and automata
Related Items
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
- 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
- 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
