A lower bound for intuitionistic logic

DOI10.1016/J.APAL.2007.01.001MaRDI QIDQ876385zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(17)

• Proof complexity of substructural logics
• Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies
• On lengths of proofs in non-classical logics
• Towards NP-P via proof complexity and search
• A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits
• Quantitative Comparison of Intuitionistic and Classical Logics - Full Propositional System
• Generalisation of proof simulation procedures for Frege systems by M. L. Bonet and S. R. Buss
• Substitution Frege and extended Frege proof systems in non-classical logics
• Lower bounds for invariant queries in logics with counting.
• Proof complexity of non-classical logics
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• Lower bounds for modal logics
• scientific article; zbMATH DE number 5161489 (Why is no real title available?)
• Proof complexity of intuitionistic implicational formulas
• scientific article; zbMATH DE number 2187723 (Why is no real title available?)
• On the proof complexity of logics of bounded branching
• Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer)

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)