Nonstandard analysis in ACL2

DOI10.1023/A:1011908113514MaRDI QIDQ5956117zbMATH OpenOpenAlexFDO

Authors Ruben A. Gamboa, Matt Kaufmann

Publication date 19 February 2002

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1011908113514

zbMATH Keywords

ACL2automated theorem proverCommon Lispcomplex numbersirrational numbersnonstandard analysisreal numbers

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard models in mathematics (03H05)

Recommendations

• Theory extension in ACL2(r)
• Linear and nonlinear arithmetic in ACL2
• Mechanizing Nonstandard Real Analysis
• scientific article; zbMATH DE number 2101985
• Constructing the real numbers in HOL

Cited in

(18)

• Coquelicot: a user-friendly library of real analysis for Coq
• Agent-oriented modeling of the dynamics of biological organisms
• Analysis of meeting protocols by formalisation, simulation, and verification
• Theory extension in ACL2(r)
• Formalization of real analysis: a survey of proof assistants and libraries
• Automatic differentiation in ACL2
• Formal proofs for theoretical properties of Newton's method
• Formal Verification of Exact Computations Using Newton’s Method
• Banishing ultrafilters from our consciousness
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• An ACL2 Tutorial
• A Nonstandard Functional Programming Language
• Linear and nonlinear arithmetic in ACL2
• An interpreter for quantum circuits
• Equivalence of the traditional and non-standard definitions of concepts from real analysis
• Quadratic extensions in ACL2
• Formalizing the Cholesky factorization theorem
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Nonstandard analysis in ACL2

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