This well-organized book, a sequel to a previous book called Computer-Aided Reasoning: An Approach [1], is a collection of independent case studies by different authors.

It contains 14 case studies on formal methods, written by 21 researchers from academia and industry. The editors have written three of the studies, as well as an introduction and overview, a collection of summaries of the case studies, and a section on ACL2 essentials. ACL2, which stands for “a computational logic for applicative Common Lisp,” is both a logic and a programming language, and is closely related to the Common Lisp programming language. The editors' description of ACL2 is adequate enough to allow a person familiar with LISP to understand and work through the case studies. For those who want to learn more about the language, extensive data, including a user’s manual, is provided online via a home page: http://www.cs.utexas.edu/users/moore/acl2.

Each one of the case studies is a self-contained, formal (mathematical and computational) study of one aspect of computer aided reasoning, such as theorem proving, path finding, and so on. For example, the first study defines a function to find a path between two given nodes of a specific directed graph. The second study develops a proof methodology for ACL2 and applies it to the proof of the fundamental theorem of calculus, that is, “the derivative of the integral of a function is the function itself.” Several authors present studies on simulators to predict performance during the design of hardware and software systems. According to the authors, these simulator models in ACL2 are superior to those developed in standard computer languages such as C+ and C++. A researcher from IBM describes another language, DE Language, and provides exercises in simulators and proof algorithms. Other researchers discuss macros, trajectory evaluation, and other projects.

All the included studies are abstract mathematical and logical works that are interesting and valuable for specific cases in computer-aided reasoning. They exhibit a fair amount of reliance on the ACL2 language, which appears to be quite suited to the authors' purpose. But, while ACL2 is an interesting and powerful language, it is not the case that what can be done with ACL2 cannot be done with Lisp, C++, and others. There are other researchers working on projects for computer reasoning, problem solving, and other intellectual activity, with more of an eye toward generalization. It would be interesting to see if some of these case studies could be integrated into a multi-processor that would be closer to a human reasoning processor.