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
