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!
See introductory-challenge-problem-1 (Answer: introductory-challenge-problem-1-answer)
See introductory-challenge-problem-2 (Answer: introductory-challenge-problem-2-answer)
See introductory-challenge-problem-3 (Answer: introductory-challenge-problem-3-answer)
See introductory-challenge-problem-4 (Answer: introductory-challenge-problem-4-answer)
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.