Nonstandard analysis in ACL2

DOI10.1023/A:1011908113514zbMath0991.03018OpenAlexW1542193405MaRDI QIDQ5956117

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

nonstandard analysisACL2automated theorem proverCommon Lispcomplex numbersirrational numbersreal numbers

Mathematics Subject Classification ID

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

Related Items (12)

A Nonstandard Functional Programming Language ⋮ Formal Verification of Exact Computations Using Newton’s Method ⋮ Agent-oriented modeling of the dynamics of biological organisms ⋮ Theory extension in ACL2(r) ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ An ACL2 Tutorial ⋮ Banishing Ultrafilters from Our Consciousness ⋮ Analysis of meeting protocols by formalisation, simulation, and verification ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Automatic Differentiation in ACL2 ⋮ Formal proofs for theoretical properties of Newton's method

Uses Software

• ACL2

This page was built for publication: Nonstandard analysis in ACL2