Hi Tim. I don't have anything to add to Matt's excellent response. I too took note of the bogus thought that ACL2 might do well with finite fields. The only way I can imagine ACL2 being especially useful there is if you characterized arbitrary finite fields of some parameterized size. Particular finite bounds, e.g., 271, don't particularly help ACL2 unless it can just grind out all the cases by evaluation.
J _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
