[Axiom-developer] ACL2 and Axiom

[J Strother Moore]

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