Proof complexity of intuitionistic implicational formulas

DOI10.1016/J.APAL.2016.09.003zbMath1422.03124arXiv1512.05667OpenAlexW2211994174MaRDI QIDQ331054

Emil Jeřábek

Publication date: 26 October 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1512.05667

zbMATH Keywords

intuitionistic logicproof complexityimplicational fragment

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of proofs (03F20) Intermediate logics (03B55)

Related Items (3)

Essential structure of proofs as a measure of complexity ⋮ Admissibility in positive logics ⋮ On the proof complexity of logics of bounded branching

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Admissible rules in the implication-negation fragment of intuitionistic logic
• A lower bound for intuitionistic logic
• On lengths of proofs in non-classical logics
• Substitution Frege and extended Frege proof systems in non-classical logics
• The complexity of the disjunction and existential properties in intuitionistic logic
• Frege systems for extensible modal logics
• Positive Formulas in Intuitionistic and Minimal Logic
• Algebraizable logics
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for modal logics
• The separation theorem of intuitionist propositional calculus
• On the computational content of intuitionistic propositional proofs

This page was built for publication: Proof complexity of intuitionistic implicational formulas