Computer-Aided Reasoning: An Approach

by Kaufmann, Matt; Manolios, Panagiotis; Moore, J Strother

• ISBN13: 9780792377443
• ISBN10: 0792377443
• Format: Hardcover
• Copyright: 2000-06-01
• Publisher: Kluwer Academic Pub

Summary

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: 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. The ACL2 system has been successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, http://www.cs.utexas.edu/users/moore/acl2, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation.

Table of Contents

Preface	xiii
Introduction	1	(6)
Book Layout	2	(2)
The ACL2 System	4	(1)
Important Conventions and Information	4	(1)
Intended Audience	5	(2)
I Preliminaries	7	(14)
Overview	9	(12)
Reasoning	9	(1)
Philosophic Writing	10	(2)
System Models	12	(3)
Truth and Proofs	15	(1)
The Reasoning Engine	16	(1)
Effort Involved	17	(2)
Requirements on the User	19	(2)
II Programming	21	(54)
The Language	23	(34)
Basic Data Types	25	(6)
Expressions	31	(8)
Primitive Functions	39	(3)
The Read-Eval-Print Loop	42	(1)
Useful ACL2 Programming Commands	42	(2)
Common Recursions	44	(6)
Multiple Values	50	(1)
Guards and Type Correctness	51	(1)
Introduction to Macros	52	(3)
Declarations	55	(2)
Programming Exercises	57	(8)
Non-Recursive Definitions	57	(1)
Some Recursive Definitions	58	(3)
Tail Recursion	61	(1)
Multiple Values and Sorting	62	(1)
Mutual Recursion	63	(1)
Arrays and Single-Threaded Objects	64	(1)
Macros	65	(10)
Advice on Using Macros	65	(1)
Details on Ampersand Markers	66	(3)
Backquote	69	(2)
An Example	71	(4)
III Reasoning	75	(42)
The Logic	77	(26)
Quantifier-Free First-Order Logic	80	(3)
The Axioms of ACL2	83	(2)
The Ordinals	85	(4)
The Definitional Principle	89	(4)
The Induction Principle	93	(6)
Additional Logical Constructs	99	(4)
Proof Examples	103	(14)
Simple Example Theorems	103	(2)
Example Theorems with Induction	105	(2)
Example Theorems About Trees	107	(5)
Comments About the Proof Process	112	(2)
Exercises	114	(3)
IV Gaming	117	(106)
The Mechanical Theorem Prover	119	(36)
A Sample Session	119	(2)
Organization of the Theorem Prover	121	(17)
Simplification Revisited	138	(15)
Comments	153	(2)
How to Use the Theorem Prover	155	(28)
The Method	155	(5)
Inspecting Failed Proofs	160	(10)
Another Example	170	(4)
Finer-Grained Interaction: The ``Proof-Checker''	174	(9)
Theorem Prover Examples	183	(28)
Factorial	183	(4)
Associative and Commutative Functions	187	(4)
Insertion Sort	191	(3)
Tree Manipulation	194	(5)
Binary Adder and Multiplier	199	(4)
Compiler for Stack Machine	203	(8)
Theorem Prover Exercises	211	(12)
Starters	211	(1)
Sorting	212	(2)
Compressed Lists	214	(1)
Summations	215	(1)
Tautology Checking	216	(2)
Encapsulation	218	(1)
Permutation Revisited	219	(2)
The Extractor Problem	221	(1)
Finite Set Theory	221	(2)
Appendices	223	(34)
A Using the ACL2 System	223	(16)
A.1 Introduction	223	(1)
A.2 The Read-Eval-Print Loop	224	(3)
A.3 Managing ACL2 Sessions	227	(6)
A.4 Using the Documentation	233	(6)
B Additional Features	239	(18)
B.1 Proof/Session Management	240	(2)
B.2 Working with the Rewriter	242	(5)
B.3 Rule Classes	247	(1)
B.4 The ACL2 State and IO	248	(2)
B.5 Efficient Execution	250	(3)
B.6 Other Topics	253	(1)
B.7 Troubleshooting Guide	254	(3)
Bibliography	257	(4)
Index	261