J
Ok. Once I climb the learning curve I'll look at that
in more detail.
I've put up a git repository to contain the changes I
need to make to embed ACL2. Both Axiom and ACL2 can sit
in the same lisp image. I have to figure out some Axiom
"cover" domains that export things like a "prove" function
and a compatible set of domains to cover the data representation.
I looked at the code a bit last night. Most of the code changes
would involve things like #- conditionally removing the ACL2
user I/O and GCL initialization.
Tim
On 10/2/2010 4:29 AM, J Strother Moore wrote:
Hi Tim. You asked
Does ACL2 handle reasoning about interval arithmetic?
Are there particular books in ACL2 I should study?
I am not aware of an interval arithmetic book.
There have been several undergraduate student
projects to build simple interval arithmetic books
but none made it into the distribution. Of
course, I presume you're aware of ACL2's extensive
collection of rational and integer arithmetic
books, e.g., arithmetic-5/top and the modulo
arithmetic of ihs and the
register-transfer/floating point stuff of rtl
(most recently rtl8).
J
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
