Solutions to the Exercises

Computer-Aided Reasoning: An Approach

Our solutions are provided in plain text format rather than HTML, Postscript, PDF, or other formats. This way the solutions can be loaded into ACL2 conveniently. You may wish to enlarge your browser window to the full screen to accommodate lines containing 80 characters. Once you are in one of our solution files, you may wish to use your browser's search command to find the particular exercise for which you are looking. All of these files are part of ACL2's standard distribution (Versions 2.5 and higher). So if ACL2 is installed on your machine, you may already have local copies of these files on the ACL2 books/textbook/ subdirectory.

  1Introduction (no exercises)


  2Overview (no exercises)


  3The Language
Exercises 3.1 - 3.9
Exercises 3.10 - 3.23
  4Programming Exercises
Exercises 4.1 - 4.21 in :program mode (see note 4)
Exercises 4.1 - 4.21 in :logic mode (see note 4)
Exercises 5.1 - 5.7


  6The 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)
  7Proof Examples
Exercises 7.1 - 7.9


  8The Mechanical Theorem Prover (no exercises)
  9How to Use the Theorem Prover (no exercises)
10Theorem 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)
11Theorem 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


Note 4

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.

Note 6

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.

Note 10

Chapter 10 contains no exercises for the reader. It presents exercises and describes our solutions. We provide the scripts for those solutions here.

Note 11

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.