[Axiom-developer] Re: ACL2 and Axiom

[Tim Daly]

 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