ACL2 problems for 10/30 class
Sandip Ray
Matt Kaufmann (CCed) has graciously agreed to talk in the class on
Thursday, Oct 30, showing how to effectively use the ACL2 Theorem
Prover on a proof project. I hope that his demo will help you
understand how to effectively use ACL2 to solve your homework problems
and make progress with your projects.
To make matters concrete, Matt has suggested that you bring to class
specific proof problems that you might be having trouble doing with
ACL2. If you bring the problems on a USB device or a CD, Matt has
agreed to load them into his laptop and solve them in real-time with
ACL2, in front of the class, with class participation.
Matt writes:
If I'm given several such, I'd focus first on the most simply stated
-- so they shouldn't bring big hairy formalizations, but rather,
concisely stated proof problems.
So consider bringing for Matt crisply stated ACL2 proof problems in
class on Thursday.
Note that this pertains to difficulties you might be having with
proving your theorems _with ACL2_. In this context, recall that you
can do your unfinished proof problems from HW4 with ACL2. So if
you're facing difficulty with doing some of them with ACL2, then you
can bring them in. Also, you can bring in a specific proof problem
that you might be having in starting off with your project. In
addition, if there are proof problems that you have managed to do, but
felt there might be a simpler way to do it, then such problems are
also game.
However, if you can do a problem with ACL2, but are having
difficulties with _hand derivations_, then please _don't_ bring such
problems. Matt's lecture will focus on ACL2 proofs, not hand
derivations.
Also, recall that I have offered to do some proof problems by hand,
once you have selected a 3 representative ones. That offer still
stands, but is unrelated to Matt's request. Again, Matt's request
pertains to ACL2 proofs.
I will mention these in class tomorrow, but I thought I'd give you
guys a heads-up.
Thanks,
-- Sandip