Fundamental Proof Methods In Computer Science
A Computer-Based Approach
by Arkoudas, Musser
ISBN: 9780262364317 | Copyright 2017
Instructor Requests
| Expand/Collapse All | |
|---|---|
| Contents (pg. v) | |
| Preface (pg. xv) | |
| I Introduction (pg. 1) | |
| 1 An Overview of Fundamental Proof Methods (pg. 3) | |
| 1.1 Equality chaining (pg. 3) | |
| 1.2 Induction (pg. 8) | |
| 1.3 Case analysis (pg. 10) | |
| 1.4 Proof by contradiction (pg. 12) | |
| 1.5 Abstraction/specialization (pg. 13) | |
| 1.6 The usual case: Proof methods in combination (pg. 15) | |
| 1.7 Automated proof (pg. 15) | |
| 1.8 Structure of the book (pg. 16) | |
| 2 Introduction to Athena (pg. 19) | |
| 2.1 Interacting with Athena (pg. 22) | |
| 2.2 Domains and function symbols (pg. 23) | |
| 2.3 Terms (pg. 27) | |
| 2.4 Sentences (pg. 34) | |
| 2.5 Definitions (pg. 40) | |
| 2.6 Assumption bases (pg. 42) | |
| 2.7 Datatypes (pg. 44) | |
| 2.8 Polymorphism (pg. 50) | |
| 2.9 Meta-identifiers (pg. 61) | |
| 2.10 Expressions and deductions (pg. 62) | |
| 2.11 More on pattern matching (pg. 78) | |
| 2.12 Directives (pg. 85) | |
| 2.13 Overloading (pg. 86) | |
| 2.14 Programming (pg. 89) | |
| 2.15 A consequence of static scoping (pg. 98) | |
| 2.16 Miscellanea (pg. 99) | |
| 2.17 Summary and notational conventions (pg. 103) | |
| 2.18 Exercises (pg. 105) | |
| II Fundamental Proof Methods (pg. 111) | |
| 3 Proving Equalities (pg. 113) | |
| 3.1 Numeric equations (pg. 113) | |
| 3.2 Equality chaining preview (pg. 116) | |
| 3.3 Terms and sentences as trees (pg. 117) | |
| 3.4 The logic behind equality chaining (pg. 120) | |
| 3.5 More examples of equality chaining (pg. 128) | |
| 3.6 A more substantial proof example (pg. 130) | |
| 3.7 A better proof (pg. 134) | |
| 3.8 The principle of mathematical induction (pg. 135) | |
| 3.9 List equations (pg. 140) | |
| 3.10 Evaluation of ground terms (pg. 150) | |
| 3.11 Top-down proof development (pg. 152) | |
| 3.12 ⋆ Input expansion and output transformation (pg. 158) | |
| 3.13 ⋆ Conjecture falsification (pg. 168) | |
| 3.14 ⋆ Conditional rewriting and additional chaining features (pg. 172) | |
| 3.15 ⋆ Proper function definitions (pg. 179) | |
| 3.16 Summary (pg. 185) | |
| 3.17 Additional exercises (pg. 186) | |
| 3.18 Chapter notes (pg. 189) | |
| 4 Sentential Logic (pg. 191) | |
| 4.1 Working with the Boolean constants (pg. 191) | |
| 4.2 Working with conjunctions (pg. 192) | |
| 4.3 Working with conditionals (pg. 194) | |
| 4.4 Working with disjunctions (pg. 199) | |
| 4.5 Working with negations (pg. 202) | |
| 4.6 Working with biconditionals (pg. 206) | |
| 4.7 Forcing a proof (pg. 207) | |
| 4.8 Putting it all together (pg. 209) | |
| 4.9 A library of useful methods for sentential reasoning (pg. 211) | |
| 4.10 Recursive proof methods (pg. 226) | |
| 4.11 Dealing with large conjunctions and disjunctions (pg. 236) | |
| 4.12 Sentential logic semantics (pg. 238) | |
| 4.13 SAT solving (pg. 246) | |
| 4.14 Proof heuristics for sentential logic (pg. 272) | |
| 4.15 ⋆ A theorem prover for sentential logic (pg. 294) | |
| 4.16 Additional exercises (pg. 304) | |
| 4.17 Chapter notes (pg. 315) | |
| 5 First-Order Logic (pg. 319) | |
| 5.1 Working with universal quantifications (pg. 323) | |
| 5.2 Working with existential quantifications (pg. 331) | |
| 5.3 Some examples (pg. 338) | |
| 5.4 Methods for quantifier reasoning (pg. 342) | |
| 5.5 Proof heuristics for first-order logic (pg. 353) | |
| 5.6 First-order logic semantics (pg. 372) | |
| 5.7 Additional exercises (pg. 385) | |
| 5.8 Chapter notes (pg. 393) | |
| 6 Implication Chaining (pg. 395) | |
| 6.1 Implication chains (pg. 395) | |
| 6.2 Using sentences as justifiers (pg. 402) | |
| 6.3 Implication chaining through sentential structure (pg. 409) | |
| 6.4 Using chains with chain-last (pg. 411) | |
| 6.5 Backward chains and chain-first (pg. 413) | |
| 6.6 Equivalence chains (pg. 415) | |
| 6.7 Mixing equational, implication, and equivalence steps (pg. 417) | |
| 6.8 Chain nesting (pg. 421) | |
| 6.9 Exercises (pg. 423) | |
| III Proofs About Fundamental Datatypes (pg. 427) | |
| 7 Organizing Theory Development with Athena Modules (pg. 429) | |
| 7.1 Introducing a module (pg. 429) | |
| 7.2 Natural numbers using modules (pg. 431) | |
| 7.3 Extending a module (pg. 433) | |
| 7.4 Modules for function symbols (pg. 434) | |
| 7.5 Additional module features (pg. 435) | |
| 7.6 Additional module procedures (pg. 436) | |
| 7.7 A note on indentation (pg. 437) | |
| 8 Natural Number Orderings (pg. 439) | |
| 8.1 Properties of natural number ordering functions (pg. 439) | |
| 8.2 Natural number subtraction (pg. 451) | |
| 8.3 Ordered lists (pg. 459) | |
| 8.4 Binary search trees (pg. 463) | |
| 8.5 Summary and a connecting theorem (pg. 469) | |
| 8.6 Additional exercises (pg. 472) | |
| 8.7 Chapter notes (pg. 473) | |
| 9 Integer Representations and Proof Mappings (pg. 475) | |
| 9.1 Declarations and axioms (pg. 475) | |
| 9.2 First proofs of integer properties (pg. 477) | |
| 9.3 Another integer representation (pg. 478) | |
| 9.4 Mappings between the signed and pair representations (pg. 480) | |
| 9.5 Additive homomorphism property (pg. 481) | |
| 9.6 Associativity and commutativity of integer addition (pg. 483) | |
| 9.7 Power series (pg. 484) | |
| 9.8 Summary and looking ahead (pg. 487) | |
| 9.9 Additional exercises (pg. 488) | |
| 10 Fundamental Discrete Structures (pg. 491) | |
| 10.1 Ordered pairs (pg. 493) | |
| 10.2 Options (pg. 497) | |
| 10.3 Sets, relations, and functions (pg. 499) | |
| 10.4 Maps (pg. 533) | |
| 10.5 Chapter notes (pg. 558) | |
| IV Proofs About Algorithms (pg. 561) | |
| 11 A Binary Search Algorithm (pg. 563) | |
| 11.1 Defining the algorithm (pg. 563) | |
| 11.2 First correctness properties (pg. 569) | |
| 11.3 Specifying requirements on a function to be defined (pg. 574) | |
| 11.4 Correctness of an optimized binary search algorithm (pg. 575) | |
| 11.5 Summary and looking ahead (pg. 576) | |
| 11.6 Additional exercises (pg. 577) | |
| 12 A Fast Exponentiation Algorithm (pg. 579) | |
| 12.1 Mathematical background (pg. 579) | |
| 12.2 Strong induction (pg. 581) | |
| 12.3 Properties of half (pg. 583) | |
| 12.4 Properties of odd and even (pg. 587) | |
| 12.5 Properties of power (pg. 589) | |
| 12.6 Properties of fast-power (pg. 590) | |
| 12.7 Tail recursion, a potential optimization (pg. 592) | |
| 12.8 Transforming strong induction into ordinary induction (pg. 596) | |
| 12.9 Measure induction (pg. 597) | |
| 12.10 Summary and looking ahead (pg. 599) | |
| 12.11 Additional exercises (pg. 599) | |
| 13 Euclid’s Algorithm for Greatest Common Divisors (pg. 603) | |
| 13.1 Quotient and remainder (pg. 603) | |
| 13.2 The division algorithm (pg. 605) | |
| 13.3 Divisibility (pg. 608) | |
| 13.4 Euclid’s algorithm (pg. 616) | |
| 13.5 Summary (pg. 621) | |
| 13.6 Additional exercises (pg. 621) | |
| 13.7 Chapter notes (pg. 623) | |
| V Proofs at an Abstract Level (pg. 625) | |
| 14 Abstract Structures (pg. 627) | |
| 14.1 Group properties (pg. 627) | |
| 14.2 Theory refinement (pg. 631) | |
| 14.3 Writing proofs at the level of a theory (pg. 635) | |
| 14.4 Abstract proof method conventions (pg. 638) | |
| 14.5 Dynamic evolution of theories (pg. 641) | |
| 14.6 Testing abstract proofs (pg. 642) | |
| 14.7 Group theory refinements (pg. 644) | |
| 14.8 ⋆ Permutations as a group (pg. 653) | |
| 14.9 Ordering properties at an abstract level (pg. 664) | |
| 14.10 Additional exercises (pg. 678) | |
| 15 Abstract Algorithms (pg. 683) | |
| 15.1 An abstract binary search algorithm (pg. 683) | |
| 15.2 An abstract fast-power algorithm (pg. 690) | |
| 16 Algorithms on Memory Abstractions (pg. 703) | |
| 16.1 Axioms and theorems for individual memory locations (pg. 703) | |
| 16.2 Iterators and ranges (pg. 709) | |
| 16.3 Range count algorithm (pg. 721) | |
| 16.4 Range replace algorithm (pg. 724) | |
| 16.5 Range copy algorithm (pg. 729) | |
| 16.6 Range copy-backward algorithm (pg. 734) | |
| 16.7 Adapters: Reverse-iterator and reverse-range (pg. 737) | |
| 16.8 Implementing copy-backward (pg. 740) | |
| 16.9 Random-access iterators (pg. 743) | |
| 16.10 A binary search algorithm (pg. 754) | |
| 16.11 Summary and suggestions for continued study (pg. 761) | |
| VI Proofs about Programming Languages (pg. 765) | |
| 17 A Correctness Proof for a Toy Compiler (pg. 767) | |
| 17.1 Interpreting and compiling numeric expressions (pg. 767) | |
| 17.2 Handling errors explicitly (pg. 783) | |
| 17.3 Chapter notes (pg. 797) | |
| 18 A Simple Imperative Programming Language (pg. 799) | |
| 18.1 A simple imperative language (pg. 799) | |
| 18.2 Semantics of expressions (pg. 808) | |
| 18.3 Semantics of commands (pg. 817) | |
| 18.4 ⋆ Testing the semantics (pg. 827) | |
| 18.5 Some lemmas (pg. 833) | |
| 18.6 Reasoning about the language (pg. 844) | |
| 18.7 Chapter notes (pg. 852) | |
| Appendices (pg. 855) | |
| A Athena Reference (pg. 857) | |
| A.1 Syntax (pg. 857) | |
| A.2 Values (pg. 858) | |
| A.3 Operational semantics (pg. 861) | |
| A.4 Pattern matching (pg. 875) | |
| A.5 Selectors (pg. 881) | |
| A.6 Prefix syntax (pg. 882) | |
| B Logic Programming and Prolog (pg. 885) | |
| B.1 Basics of logic programming (pg. 885) | |
| B.2 Examples (pg. 888) | |
| B.3 Implementing a Prolog interpreter (pg. 893) | |
| B.4 Integration with external Prolog systems (pg. 898) | |
| B.5 Automating the handling of equations (pg. 902) | |
| C Pizza, Recursion, and Induction (pg. 905) | |
| C.1 Representing and reasoning about pizzas (pg. 905) | |
| C.2 Polymorphic pizzas (pg. 914) | |
| D Automated Theorem Proving (pg. 919) | |
| D.1 General automated theorem proving (pg. 920) | |
| D.2 SMT solving (pg. 934) | |
| E Solutions to Selected Exercises (pg. 945) | |
| Chapter 2 (pg. 945) | |
| Chapter 3 (pg. 949) | |
| Chapter 4 (pg. 958) | |
| Chapter 5 (pg. 1010) | |
| Chapter 6 (pg. 1032) | |
| Chapter 7 (pg. 1034) | |
| Chapter 8 (pg. 1035) | |
| Chapter 9 (pg. 1049) | |
| Chapter 10 (pg. 1055) | |
| Chapter 11 (pg. 1072) | |
| Chapter 12 (pg. 1078) | |
| Chapter 13 (pg. 1081) | |
| Chapter 14 (pg. 1083) | |
| Chapter 15 (pg. 1107) | |
| Chapter 16 (pg. 1110) | |
| Chapter 17 (pg. 1126) | |
| Chapter 18 (pg. 1131) | |
| References (pg. 1159) | |
| Glossary (pg. 1165) | |
| Index (pg. 1175) | |
Konstantine Arkoudas
Konstantine Arkoudas is a Senior Research Scientist and Software Architect at Bloomberg.
David Musser
David Musser is Professor Emeritus of Computer Science at Rensselaer Polytechnic Institute.
| Instructors Only | |
|---|---|
|
You must have an instructor account and submit a request to access instructor materials for this book.
|
|
eTextbook
Go paperless today! Available online anytime, nothing to download or install.
Features
|
