[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Re: ACL2/Axiom recommendations
From: |
Matt Kaufmann |
Subject: |
[Axiom-developer] Re: ACL2/Axiom recommendations |
Date: |
Sat, 23 Feb 2008 20:23:54 -0600 |
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