Skip to Main content Skip to Navigation
Conference papers

A Note on the Complexity of Classical and Intuitionistic Proofs

Matthias Baaz 1 Alexander Leitsch 1 Giselle Reis 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : —We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers (those without eigenvariable conditions): " 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) ". 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.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01208346
Contributor : Giselle Reis <>
Submitted on : Friday, October 2, 2015 - 2:20:02 PM
Last modification on : Friday, April 30, 2021 - 10:04:55 AM
Long-term archiving on: : Sunday, January 3, 2016 - 10:44:42 AM

File

complexity.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Matthias Baaz, Alexander Leitsch, Giselle Reis. A Note on the Complexity of Classical and Intuitionistic Proofs. LICS 2015 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2015, Kyoto, Japan. pp.657 - 666, ⟨10.1109/LICS.2015.66⟩. ⟨hal-01208346⟩

Share

Metrics

Record views

428

Files downloads

410