A simplified lower bound for implicational logic

We present a streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic, adapted to Gordeev and Haeusler's dag-like natural deduction.

Logic, Reasoning, and Knowledge Advanced Algebra and Logic Semantic Web and Ontologies

View graph Source

Paper

Similar papers

A SIMPLIFIED LOWER BOUND FOR IMPLICATIONAL LOGICEmil Jeřábek2025 · Bulletin of Symbolic Logic In Library

Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logicEdward Hermann Hæusler2020 · arXiv (Cornell University) In Library

A Closer Look at Some Recent Proof Compression-Related ClaimsMichael C. Chavrimootoo, Ethan Ferland, Erin M. Gibson et al.2022 · arXiv (Cornell University) In Library

On the horizontal compression of dag-derivations in minimal purely implicational logicEdward Hermann Hæusler, José Flávio Cavalcante Barros Junior, Robinson2022 · arXiv (Cornell University) In Library

Applying Saturation-Based Theorem Proving to Open Problems in Positive Implicational LogicBranden Fitelson, Nicolas Peltier2026 · Journal of Automated Reasoning In Library

Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)Christian Alrabbaa, F. Baader, S. Borgwardt et al.2020 · Logic Programming and Automated Reasoning · 48 citations In Library

Finding Small Proofs for Description Logic Entailments: Theory and PracticeChristian Alrabbaa, Franz Baader, Stefan Borgwardt et al.2020 · EPiC series in computing In Library

Yet another argument in favour of NP=CoNPEdward Hermann Hæusler2020 · arXiv (Cornell University) In Library

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic LogicGuido Fiorino2021 · arXiv (Cornell University) In Library

A Fundamental Non-Classical LogicWesley H. Holliday2023 · Logics In Library

Source of record

OpenAlex

44B

Welcome.

This panel sticks with you. Pick anything below and it opens right beside it, so you can dig through 60,000-plus records without ever losing your spot here.

Travel 44B

LibraryPapers, policy, standards, statute LabsEvery organization building AI ModelsIntelligence, price, and speed BenchmarksThe evaluation catalog IncidentsAI failures and harms SearchOne field across everything DashboardThe state of AI accountability in NY 44B RegistryThe Art. 44-B compliance portal