|
|
|---|
|
|
|
|---|
M. Kaufmann, P. Manolios, J S. Moore, Computer-Aided
Reasoning: An Approach, Kluwer Academic Publishers, 2000.
Relevance: introduction to ACL2
This book explains how to program in the ACL2 functional programming language, how that language is formalized as a logic, and how to use the theorem prover. While the language and logic have acquired additional features in subsequent years, most new features are orthogonal to the system described here. Thus, the system here describes a subset of the functionality of the current version of ACL2. Probably the single most “incompatible” addition was the change of representation of the ordinals. But the Errata published online in the link above explains how to restore the default representation assumed in the book. Thus, this is an excellent beginner's introduction to how to use the system. In contains many exercises and the solutions are available online.