It seems that BDDs have been studied rather extensively in ACL2. I think the most productive approach might be to implement a BDD domain in Axiom and then applying ACL2 to the new domain. This will have the effect of bring Axiom "closer" to ACL2 and minimizing the learning distance for getting questions answered, as well as the distance to getting an effective first proof.
I've found several BDD libraries. Is there one you use and prefer? Tim _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
