caa a22 4500 463182685 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070501xx s 000 0 eng 10.1007/s10817-006-9043-0 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9043-0 Theory Extension in ACL2(r) [Elektronische Daten] [R. Gamboa, J. Cowles] ACL2(r) is a modified version of the theorem prover ACL2 that adds support for the irrational numbers using nonstandard 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). Springer Science+Business Media, Inc., 2006 ACL2(r) nationallicence theorem proving nationallicence nonstandard analysis nationallicence Gamboa R. Department of Computer Science, University of Wyoming, 82070, Laramie, WY, USA aut Cowles J. Department of Computer Science, University of Wyoming, 82070, Laramie, WY, USA aut Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 273-301 0168-7433 38:4<273 2007 38 10817 https://doi.org/10.1007/s10817-006-9043-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9043-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Gamboa R. Department of Computer Science, University of Wyoming, 82070, Laramie, WY, USA aut NATIONALLICENCE 700 1- Cowles J. Department of Computer Science, University of Wyoming, 82070, Laramie, WY, USA aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 273-301 0168-7433 38:4<273 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer