Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Do each of the problems. In each case, start with a fresh ACL2 (or undo all effects of
previous events with :ubt! 1). This may require that you ``re-discover'' the same
lemma more than once in different problems, but recognizing the need for something you
used in some previous project is part of the training.
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.
