books/textbook/ subdirectory.
| 1 | Introduction (no exercises) |
I | Preliminaries |
| 2 | Overview (no exercises) |
II | Programming |
| 3 | The Language |
| Exercises 3.1 - 3.9 | |
| Exercises 3.10 - 3.23 | |
| 4 | Programming Exercises |
Exercises 4.1 - 4.21
in :program mode (see note 4) | |
Exercises 4.1 - 4.21
in :logic mode (see note 4) | |
| 5 | Macros |
| Exercises 5.1 - 5.7 | |
III | Reasoning |
| 6 | The Logic |
| Exercises 6.1 - 6.25 with pencil and paper (see note 6) | |
| Exercises 6.3, 6.4, 6.6 - 6.8, 6.11 - 6.16 with ACL2 (see note 6) | |
| 7 | Proof Examples |
| Exercises 7.1 - 7.9 | |
IV | Gaming |
| 8 | The Mechanical Theorem Prover (no exercises) |
| 9 | How to Use the Theorem Prover (no exercises) |
| 10 | Theorem Prover Examples (see note 10) |
|
10.1 Factorial (script) 10.2 Associative and Commutative Functions (script) 10.3 Insertion Sort (script) 10.4 Tree Manipulation (script) 10.5 Binary Adder and Multiplier (script) 10.6 Compiler for Stack Machine (script and package definition) | |
| 11 | Theorem Prover Exercises (see note 11) |
| Exercises 11.1-11.4 | |
| Exercise 11.5 | |
| Exercises 11.6 - 11.7 | |
| Exercises 11.8 - 11.14 | |
| Exercises 11.15 - 11.16 | |
| Exercises 11.17 - 11.25 | |
| Exercises 11.26 - 11.33 | |
| Exercises 11.26 - 11.33, using an arithmetic book | |
| Exercises 11.34 - 11.41 | |
| Exercises 11.42 - 11.46 | |
| Exercises 11.47 - 11.51 via approach 1 | |
| Exercises 11.47 - 11.51 via approach 2 | |
| Exercise 11.52 via approach 1 | |
| Exercise 11.52 via approach 2 | |
| Exercises 11.53 - 11.57 |
At the beginning of Chapter 4, Programming Exercises, we say that all of these exercises may be done in program mode. We also suggest that once you have learned to use the ACL2 theorem prover, you do these exercises again, this time operating in logic mode and adding and verifying guards.
We therefore have two solution files. In the first, we use
:program mode whenever ACL2 cannot automatically admit our
definitions. In the second, we use :logic mode (where possible), we
include guards with our definitions, and we verify the guards.
Many of the exercises in Chapter 6 require you to present formal proofs in terms of the primitive rules of inference or require set theoretic or other metatheoretic arguments. Such exercises do not readily admit solutions expressed as ACL2 commands.
However, a few of the exercises do admit solution with ACL2, even though you -- the reader -- are not actually expected to do them this way. Indeed, upon your first reading of Chapter 6, you will probably not be able to use the theorem prover well enough to do these proofs. But you might eventually return to these exercises with the theorem prover behind you and appreciate these solutions.
Chapter 10 contains no exercises for the reader. It presents exercises and describes our solutions. We provide the scripts for those solutions here.
We provide more than one solution for some exercises. This is just a matter of taste. Different authors prefer different styles. Sometimes, one solution is less elegant than another but more clearly indicates how the solution was discovered.