ACL2 proof automation is already in place. With this latest push every function in every category, domain, and package has an attached signature. Every function is automatically pushed through COQ, only as a comment form at the moment. Function proofs can be automated by lifting them out of the comment section which leads to an incremental strategy.
There appear to be about 14000+ algebra functions so this effort will take a few weeks :-) The next step is to choose functions to prove. Initially this seems like one of three choices: 1 choose functions that are trivial (e.g. == false) 2 choose functions that are covers for underlying lisp code 3 choose a domain, e.g. List Choice 1 seems easiest to prove and will likely be an initial step. Choice 2 has the advantage that the underlying lisp code can be proven in ACL2 and the algebra level by COQ. This demonstrates the synergy between the two system when used in Axiom. Choice 3 attacks a domain that seems well studied in the COQ literature. In any case, the preparations are in place. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer