A proof-search procedure for intuitionistic propositional logic

DOI10.1007/s00153-013-0342-yzbMath1302.03034OpenAlexW2023242314MaRDI QIDQ377482

R. Alonderis

Publication date: 6 November 2013

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-013-0342-y

zbMATH Keywords

sequent calculuspropositional intuitionistic logicGlivenko's theorem

Mathematics Subject Classification ID

Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of proofs (03F20)

Uses Software

• leanCoP
• ileanCoP
• Pesca

Cites Work

• On the intuitionistic force of classical search
• Glivenko Classes of Sequents for Propositional Star-Free Likelihood Logic
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• A Connection-Based Characterization of Bi-intuitionistic Validity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item