Elements of mathematical analysis in PVS

DOI10.1007/BFB0105402MaRDI QIDQ6567709zbMATH OpenFDO

Authors Bruno Dutertre

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105402

Mathematics Subject Classification ID

Continuity and related questions (modulus of continuity, semicontinuity, discontinuities, etc.) for real functions in one variable (26A15) Formalization of mathematics in connection with theorem provers (68V20) Differentiation (real functions of one variable): general theory, generalized derivatives, mean value theorems (26A24) Foundations: limits and generalizations, elementary topology of the line (26A03)

Recommendations

• scientific article; zbMATH DE number 2000404
• Formalization of the integral calculus in the PVS theorem prover
• Formalization of real analysis: a survey of proof assistants and libraries
• scientific article; zbMATH DE number 1670744
• Applications of real number theorem proving in PVS

Cites work

• scientific article; zbMATH DE number 2185690 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3256626 (Why is no real title available?)
• Constructing the real numbers in HOL
• IMPS: An interactive mathematical proof system

This page was built for publication: Elements of mathematical analysis in PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6567709)