[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Re: ACL2 and Axiom

From: Tim Daly
Subject: [Axiom-developer] Re: ACL2 and Axiom
Date: Sat, 02 Oct 2010 11:56:02 -0400
User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv: Gecko/20100825 Thunderbird/3.1.3


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.


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).


reply via email to

[Prev in Thread] Current Thread [Next in Thread]