The undecidability of simultaneous rigid E-unification

DOI10.1016/0304-3975(96)00092-8zbMath0872.68173OpenAlexW2007520000MaRDI QIDQ671659

Andrei Voronkov, Anatoli Degtyarev

Publication date: 27 February 1997

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

Full work available at URL: https://doi.org/10.1016/0304-3975(96)00092-8

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items (14)

Monadic simultaneous rigid E-unification and related problems ⋮ Superposition-based equality handling for analytic tableaux ⋮ Free Variables and Theories: Revisiting Rigid E-unification ⋮ On quasitautologies ⋮ Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Monadic simultaneous rigid \(E\)-unification ⋮ Cyclic connections ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ A practical integration of first-order reasoning and decision procedures ⋮ What you always wanted to know about rigid E-unification ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results ⋮ Logic with equality: Partisan corroboration and shifted pairing ⋮ On the undecidability of second-order unification

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Rigid E-unification: NP-completeness and applications to equational matings
• First-order modal tableaux
• The undecidability of the second-order unification problem
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• Theorem Proving via General Matings
• Positive First-Order Logic Is NP-Complete
• Theorem proving using equational matings and rigid E -unification
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
• A completion-based method for mixed universal and rigid E-unification
• Mechanical Theorem-Proving by Model Elimination

This page was built for publication: The undecidability of simultaneous rigid E-unification