[Axiom-developer] Re: ACL2/Axiom recommendations

[Matt Kaufmann]

Hi, Tim --

Here are a couple of questions that would help me better understand
your goals.

- Why does you want to do something with BDDs if it's about "learning
  distance", rather than, say, something simpler?  For example, you
  could build a simple library about trees (write a function counting
  the number of nodes, define substitution and prove a theorem about
  how that affects the number of nodes, define a "mirror" reflecting
  function and prove that it preserves the bag of leaves, etc.).

- By "several BDD libraries" do you mean ACL2 libraries, or do you
  imagine recoding CUDD or such?  (The former makes more sense to me,
  but you might have something in mind that I'm missing.)

I think it would be particularly cool if there were ACL2-verified
applicative Lisp routines inside Axiom.  I think that's your ultimate
goal; am I right?

But I think your shorter-term goal is to learn to use ACL2 effectively
(excellent idea before getting in too deep).  In that case, I strongly
suggest that you spend time with "Recursion and Induction" and/or "How
to Prove Theorems Formally".  You can find links to these on the
"About ACL2" page of introductory and tutorial stuff at:

http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/index.html

You can skip over the easy parts and work a few exercises.  The
second, in particular, has a lot of hints on how to use the mechanical
theorem prover effectively.

-- Matt
   From: address@hidden
   Date: Sat, 23 Feb 2008 15:30:27 -0600
   Cc: address@hidden, address@hidden
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-82 required=165

   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