Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification

DOI10.1007/3-540-61511-3_67zbMath1415.03011OpenAlexW1692739636MaRDI QIDQ4647498

Andrei Voronkov

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_67

zbMATH Keywords

theorem provinginverse methodintuitionistic logicfunction symbol

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (5)

Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ The undecidability of simultaneous rigid E-unification ⋮ 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

Cites Work

• The undecidability of simultaneous rigid E-unification
• Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Special cases and substitutes for rigid \(E\)-unification
• Theorem proving using equational matings and rigid E -unification
• Proof-search in intuitionistic logic based on constraint satisfaction
• A resolution theorem prover for intuitionistic logic
• An Intuitionistic Predicate Logic Theorem Prover
• 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

This page was built for publication: Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification