Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, and theory. It is also appropriate as a reference for business and industry. In this book we present:
* A practical functional programming language closely related to Common Lisp;
* A formal logic in which defined functions correspond to axioms;
* The computer-aided reasoning system ACL2, which includes mechanical support for the proof process.
ACL2 is part of the Boyer-Moore family of theorem provers, for which its authors have received the 2005 ACM Software System Award. ACL2 has been successfully applied to projects of commercial interest, including hardware and software verification. Approximately 140 exercises are distributed throughout the book.
