Article
A proof-theoretic bound extraction theorem for CAT(κ)-spaces
Author/s | Kohlenbach, Ulrich Wilhelm
Nicolae, Adriana |
Department | Universidad de Sevilla. Departamento de Análisis Matemático |
Publication Date | 2017-06 |
Deposit Date | 2017-09-07 |
Published in |
|
Abstract | Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this ... Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this paper we adapt this to the class of CAT(κ)-spaces X for κ > 0 and establish a new metatheorem that explains specific bound extractions that recently have been achieved in this context as instances of a general logical phenomenon. |
Funding agencies | Deutsche Forschungsgemeinschaft / German Research Foundation (DFG) Dirección General de Enseñanza Superior. España |
Project ID. | KO 1737/5-2
MTM2015-65242-C2-1-P |
Citation | Kohlenbach, U.W. y Nicolae, A. (2017). A proof-theoretic bound extraction theorem for CAT(κ)-spaces. Studia Logica, 105 (3), 611-624. |
Files | Size | Format | View | Description |
---|---|---|---|---|
A proof-theoretic bound extraction ... | 286.3Kb | [PDF] | View/ | |