Errata for Computer-Aided Reasoning: An Approach (hardback)

Errata for hardback version of Computer-Aided Reasoning: An Approach

All the errors noted below have been corrected in the paperback version of the book distributed via lulu (see Ordering Information). However, if you have the Kluwer hardback version or a non-most-recent paperback version, the notes below may be helpful.

To accommodate readers of all past versions, we locate the known errors in two ways.

First, we generally give the section, paragraph, and sentence number of the sentence containing the error. In the manuscript, the first paragraph of every section is not indented; all other paragraphs are indented. We count paragraphs from 1. Text following a display (e.g., a formula or itemization) is not counted as a new paragraph unless it is indented. Sentences end with a period and are counted from 1.

The second error locator is the page number in the Kluwer hardback edition followed by the line number. Generally, each page of the Kluwer edition begins with a header containing the page number, the book or chapter title, and a horizontal line spanning the page. We count all non-blank lines below the horizontal line (i.e., we do not count the header itself and we do count all subsequent non-blank lines, whether they are part of a section title, display, or ordinary text). The hardback page and line numbers may not exactly correspond to those in the paperback versions.

Section 3.2.1, paragraph 6, sentence 1; Kluwer page 33, line 6: the phrase ``a ACL2 object'' should be ``an ACL2 object''.
Section 3.2.1, paragraph 19, sentence 2; Kluwer page 35, line 8 after Figure 3.2: the phrase ``a ACL2 object'' should be ``an ACL2 object''.
Section 4.3, paragraph 4, display after sentence 1; Kluwer page 61, lines 29 and 30: the two elided garbage collection messages should read
[SGC for 86 FIXNUM pages .. ... GC finished]
The displayed text contains LaTeX intended to produce the elipsis.
Section 6.2, paragraph 3, sentence 2; Kluwer page 83, line 20: the sentence
Analogously, (or p1 p2 ...) <==> (if p1 t (or p2 ...)), where (or p1) abbreviates p1.
should read
Analogously, (or p1 p2 ...) <==> (if p1 p1 (or p2 ...)), where (or p1) abbreviates p1.
Section 7.3, paragraph 5, sentence 1; Kluwer page 109, line 18: ``where size in measured'' should be ``where size is measured''.
Section 8.3.3, paragraph 7 (which begins with the header Types), sentence 4; Kluwer page 145, line -3 (third line from the bottom): ``{0}, {nil}, and {t}'' should be ``{0}, {nil}, and {t}.'' That is, the sentence should end with a period.
Section 8.2; Kluwer page 122: In some versions of the paperback book, Figure 8.1 is referenced but is missing. However, Figure 8.2 is the same as Figure 2.1 which appears in Section 2.5 of the paperback versions.
Section 10.6; Kluwer page 203: In versions of ACL2 after Version 2.9, we began enforcing an additional restriction on package names, namely, that lowercase alphabetic characters are not allowed in them. This requires us to change the package name used in the example of Section 10.6 from "compile" to "COMPILE". There are three places where changes have to be made.
(1) Paragraph 2, sentence 3; Kluwer page 203, line 35: the command that begins
(defpkg "compile"
should be
(defpkg "COMPILE"
(2) Paragraph 3, sentence 4; Kluwer page 204, line 8: the phrase
The above defpkg defines the new symbol package compile
should be
The above defpkg defines the new symbol package COMPILE

(3) Paragraph 3, after sentence 4; Kluwer page 204, line 11: the command
(in-package "compile")
should be
(in-package "COMPILE")
Section 11.1, Exercise 11.2; Kluwer page 211, last line of page: Exercise 11.2 references pages 49 and 115. The correct references are Kluwer pages 107 and 115.
Section 11.2, Exercise 11.5; Kluwer page 213, line 4: there is a missing ``)'' at the end of the item that begins ``Use :trans1 to print ...''
Section 11.7, Exercise 11.49; Kluwer page 220, line 5: Exercise 11.49 is simply wrong. The formula alleged not to be a theorem is a theorem, so no counterexample is possible! What we had in mind has nothing to do with mergesort but instead is an observation about perm, how-many, and quantification. The exercise should have been:
Exercise 11.49 The following is a theorem in a suitable logic permitting ACL2 terms and first-order quantification.
```
  (perm a b)
<->
  (ALL e (equal (how-many e a)
                (how-many e b)))
```
Here, by ALL we mean the universal quantifier conventionally written with an upside down A. The universal quantifier in the above theorem is crucial! The similar looking ACL2 formula
```
(iff (perm a b)
     (equal (how-many e a)
            (how-many e b)))
```
is not a theorem. Exhibit a counterexample.