Axiomatic Events in
ACL2(r): A Story of defun, defun-std, and encapsulate
Download:
PDF.
"Axiomatic Events in
ACL2(r): A Story of defun, defun-std, and encapsulate" by Ruben Gamboa, John Cowles and Nadya Kuzmina. In ACL2 Workshop 2004,
Austin, 2004.
Abstract
ACL2(r) is a variant of ACL2 that has support for reasoning about
the real and complex numbers. It is based on the logic of non-standard
analysis, axiomatized by Nelson as an extension of ZF set theory.
This paper lays out the logical foundations of ACL2(r).
Download:
PDF.