On preserving the computational content of mathematical proofs: toy examples for a formalising strategy

DOI10.1007/978-3-030-80049-9_26MaRDI QIDQ2117791zbMATH OpenOpenAlexFDO

Authors Angeliki Koutsoukou-Argyraki

Publication date 22 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-80049-9_26

zbMATH Keywords

machine learningproof theoryIsabelle/HOLproof assistantsformalisationproof mininginteractive theorem proverscomputational content

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 6983477 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3278867 (Why is no real title available?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Computable analysis and notions of continuity in \textsc{Coq}
• Effective asymptotic regularity for one-parameter nonexpansive semigroups
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Effective rates of convergence for the resolvents of accretive operators
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• Opinion: The Mechanization of Mathematics
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Proof mining for nonlinear operator theory. Four case studies on accretive operators, the Cauchy problem and nonexpansive semigroups
• Proofs and computations
• Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators
• The computational content of classical arithmetic

Cited in

(2)

• scientific article; zbMATH DE number 1951637 (Why is no real title available?)
• A computational study of a class of recursive inequalities

Describes a project that uses

Uses Software

• HOList
• Automath
• Isabelle/HOL

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)