| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A Note on the Complexity of Classical and Intuitionistic Proofs
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.
Cited literature [9 references]
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
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)