Hi, Tim -- Cool! Sure, I can imagine reasoning about data structures and rational arithmetic of Axiom.
I don't know what "Special Functions" means, but since you mention floating point I should say that reasoning about floating point operations can be tricky -- much trickier in general, I'd say, than rational operations. That's because rationals are a primitive data type in ACL2, but floating point operations need to be implemented in terms of bit-level and rational operations (grab exponent, mantissa and sign fields; then do stuff to the corresponding rationals; then transform back to floating point). You're right that there's been work on floating point -- see directory books/rtl/rel7/lib/ that comes with ACL2 -- but still, that's relatively complex stuff I'd say. Finite fields would be a cool application, but I don't know of existing work, so you'd probably be building specifications and theorems from the ground up. You could query the acl2 or acl2-help list in case someone knows of work with ACL2 in finite fields. But the limits you mention make me wonder if a tool based more directly on decision procedures might be more appropriate -- where ACL2 could shine is in proving general properties, rather than using "brute force" to check properties of a particular finite field's addition and multiplication tables. I'm pretty bad at knowing about (or remembering) previous work, but you could try the "SEARCH" link that's near the top of the ACL2 home page, or query the mailing list(s) as mentioned above. I hope this helps. If you haven't used ACL2, you might want to look at some introductory materials such as: - The "Tours", "demos", and "Hyper-Card" links on the home page - The topic ACL2-TUTORIAL in the user's manual - The ACL2 books, especially "Computer-Aided Reasoning: An Approach" (see http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books) - The introductory and tutorial stuff at http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/index.html -- Matt From: [EMAIL PROTECTED] Date: Fri, 22 Feb 2008 15:13:24 -0600 Cc: [EMAIL PROTECTED], [email protected] X-SpamAssassin-Status: No, hits=-2.6 required=5.0 X-UTCS-Spam-Status: No, hits=-82 required=165 Matt and J, I've been looking at ACL2 in order to look at proving Axiom programs correct. Besides the proof mechanism, ACL2 has the desirable property that it can co-exist with Axiom in the same image and thus have direct access to internal Axiom data structures. The idea would be to decorate domains with theorems and look at automatically propagating the theorems, bringing theorems in and out of scope, based on the hierarchy. I'm undecided what the most productive area might be to concentrate upon. Perhaps you can make a suggestion. Data Structure -- this might be useful because there is a large body of literature about the issue of proving sorting correct. Rational Arithmetic -- this has properties that fit in areas that ACL2 already knows, such as the properties of abs(). Special Functions -- this has properties of manipulation of floating point values which ACL2 has already explored. Finite Fields -- this might be easier due to the limits of the size and number of elements under consideration. Given your experience can you give me some high level advice and potential pointers to previous work? Tim Daly [EMAIL PROTECTED] _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
