On the computational content of intuitionistic propositional proofs

Annals of Pure and Applied Logic 109 (1-2):49-64 (2001)
  Copy   BIBTEX


The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic propositional calculus does not always have polynomial size proofs and that the classical propositional calculus provides a superpolynomial speedup over the intuitionistic propositional calculus. The disjunction property for intuitionistic propositional logic is proved to be P-hard by a reduction to the circuit value problem



    Upload a copy of this work     Papers currently archived: 91,252

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
The Basic Intuitionistic Logic of Proofs.Sergei Artemov & Rosalie Iemhoff - 2007 - Journal of Symbolic Logic 72 (2):439 - 451.
Intuitionistic Completeness and Classical Logic.D. C. McCarty - 2002 - Notre Dame Journal of Formal Logic 43 (4):243-248.
Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.


Added to PP

27 (#560,928)

6 months
12 (#183,686)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Incompleteness in the Finite Domain.Pavel Pudlák - 2017 - Bulletin of Symbolic Logic 23 (4):405-441.
A lower bound for intuitionistic logic.Pavel Hrubeš - 2007 - Annals of Pure and Applied Logic 146 (1):72-90.
On lengths of proofs in non-classical logics.Pavel Hrubeš - 2009 - Annals of Pure and Applied Logic 157 (2-3):194-205.
Frege systems for extensible modal logics.Emil Jeřábek - 2006 - Annals of Pure and Applied Logic 142 (1):366-379.

View all 8 citations / Add more citations