A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic

DOI10.1007/978-3-030-29026-9_7zbMath1435.68367OpenAlexW2969539880MaRDI QIDQ2180511

Rajeev Goré, Camillo Fiorentini, Stéphane Graham-Lengrand

Publication date: 14 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29026-9_7

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT ⋮ Efficient SAT-based proof search in intuitionistic propositional logic ⋮ SAT-based proof search in intermediate propositional logics

Uses Software

• Unnamed Item
• Psyche
• intuit

This page was built for publication: A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic