[Axiom-developer] ACL2/Axiom recommendations

[daly]

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