On the computational content of intuitionistic propositional proofs

DOI10.1016/S0168-0072(01)00040-9zbMath1009.03027OpenAlexW2042899834MaRDI QIDQ5940143

Pavel Pudlák, Samuel R. Buss

Publication date: 22 April 2003

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

Full work available at URL: https://doi.org/10.1016/s0168-0072(01)00040-9

zbMATH Keywords

realizabilityintuitionistic logiccircuit complexityCraig interpolationcut-eliminationdisjunction propertyfeasible algorithmspolynomial timepropositional proof systems

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Subsystems of classical logic (including intuitionistic logic) (03B20) Turing machines and related notions (03D10) Complexity of proofs (03F20)

Related Items (8)

Monotone simulations of non-monotone proofs. ⋮ Proof complexity of intuitionistic implicational formulas ⋮ INCOMPLETENESS IN THE FINITE DOMAIN ⋮ Upper bounds on complexity of Frege proofs with limited use of certain schemata ⋮ Frege systems for extensible modal logics ⋮ Proof Complexity of Non-classical Logics ⋮ Substitution Frege and extended Frege proof systems in non-classical logics ⋮ On the proof complexity of logics of bounded branching

Cites Work

• Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity
• The complexity of the disjunction and existential properties in intuitionistic logic
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the computational content of intuitionistic propositional proofs