A lower bound for intuitionistic logic

DOI10.1016/J.APAL.2007.01.001zbMATH Open1115.03081OpenAlexW2017209655MaRDI QIDQ876385FDOQ876385

Authors: Pavel Hrubeš 

Publication date: 18 April 2007

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

Full work available at URL: https://doi.org/10.1016/j.apal.2007.01.001

Recommendations

• On lengths of proofs in non-classical logics
• Lower bounds for modal logics
• Bounds for cut elimination in intuitionistic propositional logic
• Proof complexity of substructural logics
• Comparison of several proof systems of intuitionistic propositional logic

zbMATH Keywords

intuitionistic logicmodal logicproof complexityFrege system

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Intermediate logics (03B55) Complexity of proofs (03F20) Complexity of computation (including implicit computational complexity) (03D15)

Cites Work

• The ellipsoid method and its consequences in combinatorial optimization
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• The monotone circuit complexity of Boolean functions
• Title not available (Why is that?)
• The complexity of the disjunction and existential properties in intuitionistic logic
• Lower bounds for modal logics
• Title not available (Why is that?)
• Intuitionistic propositional logic is polynomial-space complete
• Polynomial size proofs of the propositional pigeonhole principle
• The gap between monotone and non-monotone circuit complexity is exponential
• Title not available (Why is that?)
• Speed-Up by Theories with Infinite Models

Cited In (16)

• Lower bounds for invariant queries in logics with counting.
• Title not available (Why is that?)
• Towards NP-P via proof complexity and search
• Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
• Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• Proof complexity of non-classical logics
• Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss
• Proof complexity of substructural logics
• Title not available (Why is that?)
• On the proof complexity of logics of bounded branching
• Proof complexity of intuitionistic implicational formulas
• Lower bounds for modal logics
• Quantitative Comparison of Intuitionistic and Classical Logics - Full Propositional System
• On lengths of proofs in non-classical logics
• Substitution Frege and extended Frege proof systems in non-classical logics

This page was built for publication: A lower bound for intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q876385)