A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces

DOI10.1007/S11225-016-9702-ZzbMath1420.03140OpenAlexW2569859296MaRDI QIDQ2363506

Ulrich Kohlenbach, Adriana Nicolae

Publication date: 19 July 2017

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-016-9702-z

zbMATH Keywords

effective boundsproof mining\(\mathrm{CAT}(\kappa)\)-spaces

Mathematics Subject Classification ID

Geodesics in global differential geometry (53C22) Functionals in proof theory (03F10) Manifolds of metrics (especially Riemannian) (58D17)

Related Items (1)

A proof‐theoretic metatheorem for tracial von Neumann algebras

Cites Work

• Unnamed Item
• Unnamed Item
• Chebyshev sets in geodesic spaces
• On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces
• Halpern iteration in CAT\((\kappa)\) spaces
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Logical metatheorems for abstract spaces axiomatized in positive bounded logic
• CAT\((k)\)-spaces, weak convergence and fixed points
• Effective results on nonlinear ergodic averages in CAT spaces
• Some logical metatheorems with applications in functional analysis
• General logical metatheorems for functional analysis
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

This page was built for publication: A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces