Applied Proof Theory - Proof Interpretations and their Use in Mathematics

By Ulrich Kohlenbach. Springer Monographs in Mathematics, 2008

506 citations recorded by the source corpus.

Subfields: Computer Graphics and Computer-Aided Design, Computer Networks and Communications, Geometry and Topology

View Paper: https://www.semanticscholar.org/paper/af40fb08eef71ac0df083abeed37267c264f71e2

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computer Graphics and Computer-Aided Design

In Computer Networks and Communications

In Geometry and Topology

Citations in the corpus

Nonexpansive iterations in uniformly convex $W$-hyperbolic spaces (2008, methodology): “We refer to Kohlenbach’s book [13] for details on proof mining.”
Firmly nonexpansive mappings in classes of geodesic spaces (2012, methodology): “We refer to Kohlenbach’s book [25] for details.”
Effective metastability of Halpern iterates in CAT(0) spaces (2011, background): “Moreover, these bounds have a restricted complexity depending on the principles that are used in the proof rather than merely being computable (see [22] for a comprehensive treatment).”
LOCAL STABILITY OF ERGODIC AVERAGES (2007, background): “Our extractions of bounds can be viewed as applications of a body of proof theoretic results that fall under the heading “proof mining” (see, for example, [19, 20, 21]).”
Sequential games and optimal strategies (2011, background): “It is well-known that such principle lies in between S02-induction and S 0 1-induction, see Parsons (1970) and Kohlenbach (2008).”
PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS (2019, methodology): “WKL is equivalent to a sentence of the form ∀fN→N ∃b ≤N→N 1∀xAqf (f, b, x) and can be added to the system via a Skolem constant B with the purely universal axiom ∀f, x(Bf ≤ 1 ∧ Aqf (f,Bf, x)) which is satisfiable in the full set-theoretic model and B is trivially majorized by the constant-1 function”
Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces (2007, background): “In this respect the current paper continues a case study in the general program of ‘proof mining’ which is concerned with the extraction of effective uniform bounds from (prima-facie) ineffective proofs (see the discussion in section 5 and [14] for a survey as well as [15]).”