Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
From MaRDI portal
Publication:5450521
DOI10.1007/978-3-540-77533-1zbMath1158.03002OpenAlexW561202933MaRDI QIDQ5450521
Publication date: 12 March 2008
Published in: Springer Monographs in Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-77533-1
proof theorynonlinear analysisapproximation theoryproof miningfunctional interpretationrealizibilityproof interpretation
Fixed-point theorems (47H10) Contraction-type mappings, nonexpansive mappings, (A)-proper mappings, etc. (47H09) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Approximation by polynomials (41A10) Uniqueness of best approximation (41A52) Foundations of classical theories (including reverse mathematics) (03B30) Functionals in proof theory (03F10) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items (only showing first 100 items - show all)
Ceres in intuitionistic logic ⋮ A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces ⋮ An approximate Herbrand’s theorem and definable functions in metric structures ⋮ Quantitative analysis of a subgradient-type method for equilibrium problems ⋮ An abstract proximal point algorithm ⋮ Reverse mathematics and parameter-free transfer ⋮ A footnote to ``The crisis in contemporary mathematics ⋮ Iterative approximation to a coincidence point of two mappings ⋮ Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces ⋮ On Spector's bar recursion ⋮ Between Turing and Kleene ⋮ Effective results on a fixed point algorithm for families of nonlinear mappings ⋮ Term extraction and Ramsey's theorem for pairs ⋮ On extracting variable Herbrand disjunctions ⋮ Abstract strongly convergent variants of the proximal point algorithm ⋮ Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started ⋮ Existence and convergence of fixed points for mappings of asymptotically nonexpansive type in uniformly convex W-hyperbolic spaces ⋮ A uniform betweenness property in metric spaces and its role in the quantitative analysis of the ``lion-man game ⋮ A parametrised functional interpretation of Heyting arithmetic ⋮ The strength of countable saturation ⋮ Program extraction for 2-random reals ⋮ Effective metastability for modified Halpern iterations in CAT(0) spaces ⋮ Fluctuations, effective learnability and metastability in analysis ⋮ A universal algorithm for Krull's theorem ⋮ Asymptotic behavior of averaged and firmly nonexpansive mappings in geodesic spaces ⋮ Quantitative inconsistent feasibility for averaged mappings ⋮ Equivalence of bar induction and bar recursion for continuous functions with continuous moduli ⋮ The equivalence of bar recursion and open recursion ⋮ Some principles weaker than Markov's principle ⋮ Eliminating disjunctions by disjunction elimination ⋮ Arithmetical conservation results ⋮ To be or not to be constructive, that is not the question ⋮ A nonstandard approach to asymptotic fixed point theorems ⋮ The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma ⋮ The asymptotic behavior of the composition of firmly nonexpansive mappings ⋮ On quantitative versions of theorems due to F. E. Browder and R. Wittmann ⋮ On the disjunctive Markov principle ⋮ A quantitative nonlinear strong ergodic theorem for Hilbert spaces ⋮ A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory ⋮ Rates of convergence for iterative solutions of equations involving set-valued accretive operators ⋮ Bit-complexity of classical solutions of linear evolutionary systems of partial differential equations ⋮ Logical metatheorems for abstract spaces axiomatized in positive bounded logic ⋮ On the independence of premiss axiom and rule ⋮ The bounded functional interpretation of bar induction ⋮ Primitive recursion and the chain antichain principle ⋮ Computability of finite-dimensional linear subspaces and best approximation ⋮ On modified Halpern and Tikhonov-Mann iterations ⋮ Proof mining and effective bounds in differential polynomial rings ⋮ A constructive analysis of learning in Peano arithmetic ⋮ Delimited control operators prove double-negation shift ⋮ Gödel functional interpretation and weak compactness ⋮ Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces ⋮ Classical consequences of continuous choice principles from intuitionistic analysis ⋮ A note on non-classical nonstandard arithmetic ⋮ Characterising Brouwer's continuity by bar recursion on moduli of continuity ⋮ Intuitionistic fixed point logic ⋮ Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators ⋮ Quantitative image recovery theorems ⋮ From (Idealized) exact causality-preserving transformations to practically useful approximately-preserving ones: a general approach ⋮ A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space ⋮ An application of proof mining to nonlinear iterations ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Convergence theorems of a modified iteration process for generalized nonexpansive mappings in hyperbolic spaces ⋮ Effective asymptotic regularity for one-parameter nonexpansive semigroups ⋮ Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness ⋮ The abstract type of the real numbers ⋮ On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces ⋮ Bar recursion over finite partial functions ⋮ Toward a clarity of the extreme value theorem ⋮ Completeness: when enough is enough ⋮ The computational content of arithmetical proofs ⋮ Effective results on compositions of nonexpansive mappings ⋮ On the asymptotic behavior of odd operators ⋮ Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces ⋮ On the form of witness terms ⋮ A functional interpretation for nonstandard arithmetic ⋮ Effective metastability of Halpern iterates in \(CAT(0)\) spaces ⋮ Using Ramsey's theorem once ⋮ Quantitative results on a Halpern-type proximal point algorithm ⋮ On Brouwer's continuity principle ⋮ Rates of metastability for iterations on the unit interval ⋮ The metamathematics of ergodic theory ⋮ Metastability of the proximal point algorithm with multi-parameters ⋮ Reverse formalism 16 ⋮ Pincherle's theorem in reverse mathematics and computability theory ⋮ Quantitative translations for viscosity approximation methods in hyperbolic spaces ⋮ Moduli of regularity and rates of convergence for Fejér monotone sequences ⋮ A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces ⋮ On the removal of weak compactness arguments in proof mining ⋮ The strength of compactness in computability theory and nonstandard analysis ⋮ On Goodman realizability ⋮ Explicit polynomial bounds on prime ideals in polynomial rings over fields ⋮ Nonstandardness and the bounded functional interpretation ⋮ Parallelizations in Weihrauch reducibility and constructive reverse mathematics ⋮ Quantitative coding and complexity theory of compact metric spaces ⋮ Quantitative results for Halpern iterations of nonexpansive mappings ⋮ On false Heine/Borel compactness principles in proof mining ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy ⋮ An algorithmic version of Zariski's lemma
This page was built for publication: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
