Buy it now
Buying options
Tax calculation will be finalised at checkout
Other ways to access
This is a preview of subscription content, log in via an institution to check for access.
Table of contents (11 chapters)
-
Front Matter
-
Introduction
-
Programming
-
Front Matter
-
-
Reasoning
-
Front Matter
-
-
Back Matter
About this book
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.
Authors and Affiliations
-
Advanced Micro Devices, Inc., India
Matt Kaufmann
-
The University of Texas at Austin, USA
Panagiotis Manolios, J. Strother Moore
Bibliographic Information
Book Title: Computer-Aided Reasoning
Book Subtitle: An Approach
Authors: Matt Kaufmann, Panagiotis Manolios, J. Strother Moore
Series Title: Advances in Formal Methods
DOI: https://doi.org/10.1007/978-1-4615-4449-4
Publisher: Springer New York, NY
-
eBook Packages: Springer Book Archive
Copyright Information: Springer Science+Business Media New York 2000
eBook ISBN: 978-1-4615-4449-4Published: 06 December 2012
Series ISSN: 1567-7338
Edition Number: 1
Number of Pages: XV, 270
Topics: Artificial Intelligence, Artificial Intelligence, Programming Languages, Compilers, Interpreters, Software Engineering/Programming and Operating Systems, Computer Science, general