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)
Reverse mathematics and Weihrauch analysis motivated by finite complexity theory ⋮ Proof Theory in Philosophy of Mathematics ⋮ Bounds for a nonlinear ergodic theorem for Banach spaces ⋮ Reverse Mathematics: The Playground of Logic ⋮ A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH ⋮ Measure theory and higher order arithmetic ⋮ 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 ⋮ Light monotone Dialectica methods for proof mining ⋮ 2009 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '09 ⋮ Towards Computational Complexity Theory on Advanced Function Spaces in Analysis ⋮ Rates of Convergence for Asymptotically Weakly Contractive Mappings in Normed Spaces ⋮ Firmly nonexpansive mappings in classes of geodesic spaces ⋮ Intuitionistic Provability versus Uniform Provability in $$\mathsf{RCA}$$ ⋮ A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ 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 ⋮ A UNIFORM QUANTITATIVE FORM OF SEQUENTIAL WEAK COMPACTNESS AND BAILLON'S NONLINEAR ERGODIC 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 ⋮ Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic ⋮ A note on equality in finite‐type arithmetic ⋮ Quantitative results on Fejér monotone sequences ⋮ 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 ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ A Computable Solution to Partee’s Temperature Puzzle ⋮ Unnamed Item ⋮ Effective results on nonlinear ergodic averages in CAT spaces ⋮ SEPARATING FRAGMENTS OF WLEM, LPO, AND MP ⋮ The finitary content of sunny nonexpansive retractions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Note on the Mann Iteration fork-Strict Pseudocontractions in Banach Spaces ⋮ From Nonstandard Analysis to Various Flavours of Computability Theory ⋮ Unnamed Item ⋮ 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 ⋮ The cohesive principle and the Bolzano-Weierstraß principle ⋮ The bounded functional interpretation of the double negation shift ⋮ On proximal mappings with Young functions in uniformly convex Banach spaces ⋮ Program extraction in exact real arithmetic ⋮ A constructive interpretation of Ramsey's theorem via the product of selection functions ⋮ On Tao's “finitary” infinite pigeonhole principle ⋮ On the computational content of the Bolzano-Weierstraß Principle ⋮ INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES ⋮ Proof interpretations with truth ⋮ COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS ⋮ PROOF MINING IN Lp SPACES ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On Some Semi-constructive Theories Related to Kripke–Platek Set Theory ⋮ On the non-confluence of cut-elimination ⋮ Monoidal-closed categories of tree automata ⋮ 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 ⋮ Local stability of ergodic averages ⋮ A quantitative mean ergodic theorem for uniformly convex Banach spaces ⋮ Confined modified realizability ⋮ A note on the monotone functional interpretation ⋮ Functional interpretation and inductive definitions ⋮ Logical aspects of rates of convergence in metric spaces ⋮ Weihrauch and constructive reducibility between existence statements ⋮ Nets and reverse mathematics ⋮ Hyperbolic spaces and directional contractions ⋮ THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING ⋮ BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS ⋮ ON IDEMPOTENT ULTRAFILTERS IN HIGHER-ORDER REVERSE MATHEMATICS ⋮ Construction of Fixed Points of Asymptotically Nonexpansive Mappings in Uniformly Convex Hyperbolic Spaces ⋮ Classical provability of uniform versions and intuitionistic provability ⋮ PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC ⋮ Oscillation and the mean ergodic theorem for uniformly convex Banach spaces ⋮ Bishop-Style Constructive Reverse Mathematics ⋮ On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem ⋮ THE PREHISTORY OF THE SUBSYSTEMS OF SECOND-ORDER ARITHMETIC ⋮ 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
This page was built for publication: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
