Simultaneous rigid E-unification is undecidable

DOI10.1007/3-540-61377-3_38zbMATH Open1541.03021MaRDI QIDQ6560168FDOQ6560168

Anatoli I. Degtyarev, Andrei Voronkov

Publication date: 21 June 2024

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Recursive functions and relations, subrecursive hierarchies (03D20)

Cites Work

• Linear logic
• Title not available (Why is that?)
• The foundations of mathematics. A study in the philosophy of science
• Positive First-Order Logic Is NP-Complete
• Theorem Proving via General Matings
• On Matrices with Connections
• Mechanical Theorem-Proving by Model Elimination
• The undecidability of the second-order unification problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem proving using equational matings and rigid E -unification
• Title not available (Why is that?)
• A completion-based method for mixed universal and rigid E-unification
• Title not available (Why is that?)
• The undecidability of simultaneous rigid E-unification
• Rigid E-unification: NP-completeness and applications to equational matings
• An algorithm for reasoning about equality
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: Simultaneous rigid E-unification is undecidable

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