Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
From MaRDI portal
Publication:5450521
DOI10.1007/978-3-540-77533-1zbMath1158.03002MaRDI 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 theory; nonlinear analysis; approximation theory; proof mining; functional interpretation; realizibility; proof interpretation
47H10: Fixed-point theorems
47H09: Contraction-type mappings, nonexpansive mappings, (A)-proper mappings, etc.
03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
41A10: Approximation by polynomials
41A52: Uniqueness of best approximation
03B30: Foundations of classical theories (including reverse mathematics)
03F10: Functionals in proof theory
03F03: Proof theory in general (including proof-theoretic semantics)
Related Items
Quantitative results on Fejér monotone sequences, On proximal mappings with Young functions in uniformly convex Banach spaces, INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, BOUNDS FOR INDEXES OF NILPOTENCY IN COMMUTATIVE RING THEORY: A PROOF MINING APPROACH, A Rate of Metastability for the Halpern Type Proximal Point Algorithm, Weihrauch and constructive reducibility between existence statements, Nets and reverse mathematics, Hyperbolic spaces and directional contractions, THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING, Construction of Fixed Points of Asymptotically Nonexpansive Mappings in Uniformly Convex Hyperbolic Spaces, PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC, Bishop-Style Constructive Reverse Mathematics, On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem, Reverse mathematics and Weihrauch analysis motivated by finite complexity theory, A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH, ON THE UNCOUNTABILITY OF, Revisiting jointly firmly nonexpansive families of mappings, A Nonstandard Functional Programming Language, Quadratic rates of asymptotic regularity for the Tikhonov–Mann iteration, Unnamed Item, Converse extensionality and apartness, Rates of Convergence for Asymptotically Weakly Contractive Mappings in Normed Spaces, A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC, Unnamed Item, Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, A note on equality in finite‐type arithmetic, The finitary content of sunny nonexpansive retractions, On Tao's “finitary” infinite pigeonhole principle, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, PROOF MINING IN Lp SPACES, On Some Semi-constructive Theories Related to Kripke–Platek Set Theory, Monoidal-closed categories of tree automata, BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS, ON IDEMPOTENT ULTRAFILTERS IN HIGHER-ORDER REVERSE MATHEMATICS, Classical provability of uniform versions and intuitionistic provability, Oscillation and the mean ergodic theorem for uniformly convex Banach spaces, THE PREHISTORY OF THE SUBSYSTEMS OF SECOND-ORDER ARITHMETIC, 2009 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '09, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Program extraction in exact real arithmetic, A constructive interpretation of Ramsey's theorem via the product of selection functions, Bounds for a nonlinear ergodic theorem for Banach spaces, Unnamed Item, Decidable fan theorem and uniform continuity theorem with continuous moduli, König's lemma, weak König's lemma, and the decidable fan theorem, Primitive recursive reverse mathematics, Old and new challenges in Hadamard spaces, On Korpelevich's extragradient algorithm, EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES, A computational study of a class of recursive inequalities, Bounds on strong unicity for Chebyshev approximation with bounded coefficients, Refining the arithmetical hierarchy of classical principles, A note on the finitization of Abelian and Tauberian theorems, A proof‐theoretic metatheorem for tracial von Neumann algebras, Coding of real‐valued continuous functions under WKL$\mathsf {WKL}$, Choice and independence of premise rules in intuitionistic set theory, Rates of convergence for the asymptotic behavior of second-order Cauchy problems, Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Strong Convergence for the Alternating Halpern–Mann Iteration in CAT(0) Spaces, Homotopy type theory and Voevodsky’s univalent foundations, A Computable Solution to Partee’s Temperature Puzzle, Effective results on nonlinear ergodic averages in CAT spaces, SEPARATING FRAGMENTS OF WLEM, LPO, AND MP, A Note on the Mann Iteration fork-Strict Pseudocontractions in Banach Spaces, From Nonstandard Analysis to Various Flavours of Computability Theory, The cohesive principle and the Bolzano-Weierstraß principle, On the computational content of the Bolzano-Weierstraß Principle, Proof interpretations with truth, On the non-confluence of cut-elimination, A note on the monotone functional interpretation, Proof Theory in Philosophy of Mathematics, Reverse Mathematics: The Playground of Logic, Light monotone Dialectica methods for proof mining, Towards Computational Complexity Theory on Advanced Function Spaces in Analysis, Firmly nonexpansive mappings in classes of geodesic spaces, Intuitionistic Provability versus Uniform Provability in $$\mathsf{RCA}$$, A UNIFORM QUANTITATIVE FORM OF SEQUENTIAL WEAK COMPACTNESS AND BAILLON'S NONLINEAR ERGODIC THEOREM, Well Quasi-orders and the Functional Interpretation, The Monotone Completeness Theorem in Constructive Reverse Mathematics, From Mathesis Universalis to Provability, Computability, and Constructivity, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Local stability of ergodic averages, Confined modified realizability, Measure theory and higher order arithmetic, The bounded functional interpretation of the double negation shift, A quantitative mean ergodic theorem for uniformly convex Banach spaces, Functional interpretation and inductive definitions, Logical aspects of rates of convergence in metric spaces, Effective results on a fixed point algorithm for families of nonlinear mappings, Existence and convergence of fixed points for mappings of asymptotically nonexpansive type in uniformly convex W-hyperbolic spaces, Program extraction for 2-random reals, Effective metastability for modified Halpern iterations in CAT(0) spaces, Fluctuations, effective learnability and metastability in analysis, Asymptotic behavior of averaged and firmly nonexpansive mappings in geodesic spaces, The equivalence of bar recursion and open recursion, The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma, A quantitative nonlinear strong ergodic theorem for Hilbert spaces, The bounded functional interpretation of bar induction, Primitive recursion and the chain antichain principle, A constructive analysis of learning in Peano arithmetic, Delimited control operators prove double-negation shift, Gödel functional interpretation and weak compactness, Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators, Effective asymptotic regularity for one-parameter nonexpansive semigroups, On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces, Bar recursion over finite partial functions, On the asymptotic behavior of odd operators, Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces, On quantitative versions of theorems due to F. E. Browder and R. Wittmann, Computability of finite-dimensional linear subspaces and best approximation, A functional interpretation for nonstandard arithmetic, Effective metastability of Halpern iterates in \(CAT(0)\) spaces, Explicit polynomial bounds on prime ideals in polynomial rings over fields, Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces, Some principles weaker than Markov's principle, The asymptotic behavior of the composition of firmly nonexpansive mappings, On the disjunctive Markov principle, Logical metatheorems for abstract spaces axiomatized in positive bounded logic, From (Idealized) exact causality-preserving transformations to practically useful approximately-preserving ones: a general approach, On the form of witness terms, The metamathematics of ergodic theory, 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, Eliminating disjunctions by disjunction elimination, Arithmetical conservation results, To be or not to be constructive, that is not the question, Proof mining and effective bounds in differential polynomial rings, A note on non-classical nonstandard arithmetic, A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, The computational content of arithmetical proofs, On Brouwer's continuity principle, Completeness: when enough is enough, Quantitative results on a Halpern-type proximal point algorithm, Rates of metastability for iterations on the unit interval, Metastability of the proximal point algorithm with multi-parameters, Reverse formalism 16, Quantitative translations for viscosity approximation methods in hyperbolic spaces, Parallelizations in Weihrauch reducibility and constructive reverse mathematics, Quantitative coding and complexity theory of compact metric spaces, 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, Quantitative analysis of a subgradient-type method for equilibrium problems, Between Turing and Kleene, On extracting variable Herbrand disjunctions, Abstract strongly convergent variants of the proximal point algorithm, Rates of convergence for iterative solutions of equations involving set-valued accretive operators, On the independence of premiss axiom and rule, Characterising Brouwer's continuity by bar recursion on moduli of continuity, Intuitionistic fixed point logic, 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, Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness, The abstract type of the real numbers, Toward a clarity of the extreme value theorem, Effective results on compositions of nonexpansive mappings, Using Ramsey's theorem once, Pincherle's theorem in reverse mathematics and computability theory, 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, Nonstandardness and the bounded functional interpretation, Quantitative results for Halpern iterations of nonexpansive mappings, Ceres in intuitionistic logic, A proof-theoretic bound extraction theorem for \(\mathrm{CAT}(\kappa)\)-spaces, The strength of countable saturation, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces, Classical consequences of continuous choice principles from intuitionistic analysis, Quantitative image recovery theorems, An application of proof mining to nonlinear iterations, Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started, 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, A universal algorithm for Krull's theorem, Quantitative inconsistent feasibility for averaged mappings, A nonstandard approach to asymptotic fixed point theorems, A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory, Bit-complexity of classical solutions of linear evolutionary systems of partial differential equations, On modified Halpern and Tikhonov-Mann iterations, An approximate Herbrand’s theorem and definable functions in metric structures, On Spector's bar recursion, Term extraction and Ramsey's theorem for pairs
