2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2015)

Kyoto, Japan

July 6, 2015 to July 10, 2015

ISSN: 1043-6871

ISBN: 978-1-4799-8875-4

pp: 657-666

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2015.66

ABSTRACT

We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers: "There is an elementary function f such that if &#x03C6; is a cut-free LK proof of &#x22A2; A with symbol complexity &#x2264; c, then there exists a cut-free LJ proof of &#x22A2; &#x22AF &#x22AF A with symbol complexity &#x2264; f(c)". This follows from the more general result: "There is an elementary function f such that if &#x03C6; is a cut-free LK proof of A &#x22A2; with symbol complexity &#x2264; c, then there exists a cut-free LJ proof of A &#x22A2; with symbol complexity &#x2264; f(c)". The result is proved using a suitable variant of cut-elimination by resolution (CERES) and subsumption.

INDEX TERMS

Complexity theory, Calculus, Context, Merging, Computer science, Geometry

CITATION

M. Baaz, A. Leitsch and G. Reis, "A Note on the Complexity of Classical and Intuitionistic Proofs,"

*2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, Kyoto, Japan, 2015, pp. 657-666.

doi:10.1109/LICS.2015.66

CITATIONS