Computer-Aided Reasoning
An Approach
Published on 6. December 2012
XV, 270 pages
978-1-4615-4449-4 (ISBN)
Description
Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry.
Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction.
In this book we present:
Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation.
Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction.
In this book we present:
- A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions;
- A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions;
- The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process.
Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation.
More details
Other editions
Additional editions
Book
10/2012
Springer
€266.43
Article exhausted; check different version
Book
07/2000
Kluwer Academic Publishers
€266.43
Article exhausted; check different version
Content
1 Introduction.- 1.1 Book Layout.- 1.2 The ACL2 System.- 1.3 Important Conventions and Information.- 1.4 Intended Audience.- I Preliminaries.- 2 Overview.- II Programming.- 3 The Language.- 4 Programming Exercises.- 5 Macros.- III Reasoning.- 6 The Logic.- 7 Proof Examples.- IV Gaming.- 8 The Mechanical Theorem Prover.- 9 How to Use the Theorem Prover.- 10 Theorem Prover Examples.- 11 Theorem Prover Exercises.- Appendices.- A Using the ACL2 System.- A.1 Introduction.- A.2 The Read-Eval-Print Loop.- A.3 Managing ACL2 Sessions.- A.4 Using the Documentation.- B Additional Features.- B.1 Proof/Session Management.- B.2 Working with the Rewriter.- B.3 Rule Classes.- B.4 The ACL2 State and IO.- B.5 Efficient Execution.- B.6 Other Topics.- B.7 Troubleshooting Guide.
