Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
From MaRDI portal
approximation theoryfunctional interpretationnonlinear analysisproof interpretationproof miningproof theoryrealizibility
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Foundations of classical theories (including reverse mathematics) (03B30) Proof theory in general (including proof-theoretic semantics) (03F03) Functionals in proof theory (03F10) Approximation by polynomials (41A10) Uniqueness of best approximation (41A52) Contraction-type mappings, nonexpansive mappings, (A)-proper mappings, etc. (47H09) Fixed-point theorems (47H10)
Recommendations
- New Computational Paradigms
- Mathematical logic: Proof theory, constructive mathematics. Abstracts from the workshop held April 6--12, 2008.
- Mathematical logic: proof theory, type theory and constructive mathematics
- scientific article; zbMATH DE number 2174396
- scientific article; zbMATH DE number 4033738
Cited in
(only showing first 100 items - show all)- The metamathematics of ergodic theory
- Mathematical logic: Proof theory, constructive mathematics. Abstracts from the workshop held April 6--12, 2008.
- 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
- Mathematical logic: proof theory, type theory and constructive mathematics
- 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
- Homotopy type theory and Voevodsky's univalent foundations
- A Computable Solution to Partee’s Temperature Puzzle
- Effective results on nonlinear ergodic averages in \(\text{CAT}(\kappa)\) spaces
- Separating fragments of WLEM, LPO, and MP
- A note on the Mann iteration for k-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 interpretations. Theoretical and practical aspects.
- 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
- Effective results on a fixed point algorithm for families of nonlinear mappings
- Local stability of ergodic averages
- Confined modified realizability
- scientific article; zbMATH DE number 5150882 (Why is no real title available?)
- Measure theory and higher order arithmetic
- The bounded functional interpretation of the double negation shift
- Existence and convergence of fixed points for mappings of asymptotically nonexpansive type in uniformly convex W-hyperbolic spaces
This page was built for publication: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5450521)
