__Journal article:__

** Samuel R. Buss, Grigori Mints.
"The Complexity of the Disjunction and Existence Properties in
Intiotionistic Logic."
Annals of Pure and Applied Logic 99 (1999) 93-104.**

** Download: postscript or PDF.**

** Introduction: **This paper considers the
computational complexity of the disjunction and existential properties of intuitionistic
logic. We prove that the disjunction property holds feasibly for intuitionistic
propositional logic; i.e., from a proof of $A\lor B$, a proof either of~$A$ or of~$B$ can
be found in polynomial time. For intuitionistic predicate logic, we prove superexponential
lower bounds for the disjunction property, namely, there is a superexponential lower bound
on the time required, given a proof of $A\lor B$, to produce one of $A$~and~$B$ which is
true. In addition, there is superexponential lower bound on the size of terms which
fulfill the existential property of intuitionistic predicate logic. There are
superexponential upper bounds for these problems, so the lower bounds are essentially
optimal.