On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
From MaRDI portal
Publication:2117791
DOI10.1007/978-3-030-80049-9_26OpenAlexW3185513211MaRDI QIDQ2117791FDOQ2117791
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80049-9_26
machine learningproof theoryIsabelle/HOLproof assistantsformalisationproof mininginteractive theorem proverscomputational content
Cites Work
- Title not available (Why is that?)
- Proofs and Computations
- On the interpretation of non-finitist proofs–Part II
- Title not available (Why is that?)
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- On the Interpretation of Non-Finitist Proofs--Part I
- Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
- Effective asymptotic regularity for one-parameter nonexpansive semigroups
- Title not available (Why is that?)
- Effective Rates of Convergence for the Resolvents of Accretive Operators
- PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
- The computational content of classical arithmetic
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Opinion: The Mechanization of Mathematics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (2)
Uses Software
This page was built for publication: On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117791)
