The Community for Technology Leaders
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
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 φ is a cut-free LK proof of ⊢ A with symbol complexity ≤ c, then there exists a cut-free LJ proof of ⊢ &#x22AF &#x22AF A with symbol complexity ≤ f(c)". This follows from the more general result: "There is an elementary function f such that if φ is a cut-free LK proof of A ⊢ with symbol complexity ≤ c, then there exists a cut-free LJ proof of A ⊢ with symbol complexity ≤ 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
92 ms
(Ver 3.3 (11022016))