Theory Extension in ACL2(r)

ACL2(r) is a modified version of the theorem prover ACL2 that adds support for the irrational numbers using non-standard analysis. It has been used to prove basic theorems of analysis, as well as the correctness of the implementation of transcendental functions in hardware. This paper presents the logical foundations of ACL2(r). These foundations are also used to justify significant enhancements to ACL2(r).

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: Ruben Gamboa, John R. Cowles
• Keywords: ACL2, Irrational Numbers, JAR 2007, Modified Version