Challenge problems for the new ACL2 user
Do each of the problems. In each case, start with a fresh ACL2 (or
undo all effects of previous events with
We recommend that you follow The Method and consult the documentation as needed — but that you not look at our answers until you're well and truly baffled!
In addition to these explicit challenge problems designed for beginners, the ACL2 documentation has many example solutions to problems (not always phrased in the question/answer format here). If you are looking for other examples, you should consider
annotated-ACL2-scripts (Answer: the answers are given in the examples)
When you've done the problems and compared your solutions to ours, use your browser's Back Button now to return to introduction-to-the-theorem-prover.