Fundamental Proof Methods in Computer Science: A Computer-Based Approach

Description

A textbook that teaches students to read and write proofs using Athena. Proof is the primary vehicle for knowledge generation in mathematics. In computer science, proof has found an additional use: verifying that a particular system (or component, or algorithm) has certain desirable properties. This book teaches students how to read and write proofs using Athena, a freely downloadable computer language. Athena proofs are machine-checkable and written in an intuitive natural-deduction style. The book contains more than 300 exercises, most with full solutions. By putting proofs into practice, it demonstrates the fundamental role of logic and proof in computer science as no other existing text does. Guided by examples and exercises, students are quickly immersed in the most useful high-level proof methods, including equational reasoning, several forms of induction, case analysis, proof by contradiction, and abstraction/specialization. The book includes auxiliary material on SAT and SMT solving, automated theorem proving, and logic programming. The book can be used by upper undergraduate or graduate computer science students with a basic level of programming and mathematical experience. Professional programmers, practitioners of formal methods, and researchers in logic-related branches of computer science will find it a valuable reference. Contents......Page 6 Preface......Page 16 I Introduction......Page 28 1.1 Equality chaining......Page 30 1.2 Induction......Page 35 1.3 Case analysis......Page 37 1.4 Proof by contradiction......Page 39 1.5 Abstraction/specialization......Page 40 1.7 Automated proof......Page 42 1.8 Structure of the book......Page 43 2 Introduction to Athena......Page 46 2.1 Interacting with Athena......Page 49 2.2 Domains and function symbols......Page 50 2.3 Terms......Page 54 2.4 Sentences......Page 61 2.5 Definitions......Page 67 2.6 Assumption bases......Page 69 2.7 Datatypes......Page 71 2.8 Polymorphism......Page 77 2.9 Meta-identifiers......Page 88 2.10 Expressions and deductions......Page 89 2.11 More on pattern matching......Page 105 2.12 Directives......Page 112 2.13 Overloading......Page 113 2.14 Programming......Page 116 2.15 A consequence of static scoping......Page 125 2.16 Miscellanea......Page 126 2.17 Summary and notational conventions......Page 130 2.18 Exercises......Page 132 II Fundamental Proof Methods......Page 138 3.1 Numeric equations......Page 140 3.2 Equality chaining preview......Page 143 3.3 Terms and sentences as trees......Page 144 3.4 The logic behind equality chaining......Page 147 3.5 More examples of equality chaining......Page 155 3.6 A more substantial proof example......Page 157 3.7 A better proof......Page 161 3.8 The principle of mathematical induction......Page 162 3.9 List equations......Page 167 3.10 Evaluation of ground terms......Page 177 3.11 Top-down proof development......Page 179 3.12 ⋆ Input expansion and output transformation......Page 185 3.13 ⋆ Conjecture falsification......Page 195 3.14 ⋆ Conditional rewriting and additional chaining features......Page 199 3.15 ⋆ Proper function definitions......Page 206 3.16 Summary......Page 212 3.17 Additional exercises......Page 213 3.18 Chapter notes......Page 216 4.1 Working with the Boolean constants......Page 218 4.2 Working with conjunctions......Page 219 4.3 Working with conditionals......Page 221 4.4 Working with disjunctions......Page 226 4.5 Working with negations......Page 229 4.6 Working with biconditionals......Page 233 4.7 Forcing a proof......Page 234 4.8 Putting it all together......Page 236 4.9 A library of useful methods for sentential reasoning......Page 238 4.10 Recursive proof methods......Page 253 4.11 Dealing with large conjunctions and disjunctions......Page 263 4.12 Sentential logic semantics......Page 265 4.13 SAT solving......Page 273 4.14 Proof heuristics for sentential logic......Page 299 4.15 ⋆ A theorem prover for sentential logic......Page 321 4.16 Additional exercises......Page 331 4.17 Chapter notes......Page 342 5 First-Order Logic......Page 346 5.1 Working with universal quantifications......Page 350 5.2 Working with existential quantifications......Page 358 5.3 Some examples......Page 365 5.4 Methods for quantifier reasoning......Page 369 5.5 Proof heuristics for first-order logic......Page 380 5.6 First-order logic semantics......Page 399 5.7 Additional exercises......Page 412 5.8 Chapter notes......Page 420 6.1 Implication chains......Page 422 6.2 Using sentences as justifiers......Page 429 6.3 Implication chaining through sentential structure......Page 436 6.4 Using chains with chain-last......Page 438 6.5 Backward chains and chain-first......Page 440 6.6 Equivalence chains......Page 442 6.7 Mixing equational, implication, and equivalence steps......Page 444 6.8 Chain nesting......Page 448 6.9 Exercises......Page 450 III Proofs About Fundamental Datatypes......Page 454 7.1 Introducing a module......Page 456 7.2 Natural numbers using modules......Page 458 7.3 Extending a module......Page 460 7.4 Modules for function symbols......Page 461 7.5 Additional module features......Page 462 7.6 Additional module procedures......Page 463 7.7 A note on indentation......Page 464 8.1 Properties of natural number ordering functions......Page 466 8.2 Natural number subtraction......Page 478 8.3 Ordered lists......Page 486 8.4 Binary search trees......Page 490 8.5 Summary and a connecting theorem......Page 496 8.6 Additional exercises......Page 499 8.7 Chapter notes......Page 500 9.1 Declarations and axioms......Page 502 9.2 First proofs of integer properties......Page 504 9.3 Another integer representation......Page 505 9.4 Mappings between the signed and pair representations......Page 507 9.5 Additive homomorphism property......Page 508 9.6 Associativity and commutativity of integer addition......Page 510 9.7 Power series......Page 511 9.8 Summary and looking ahead......Page 514 9.9 Additional exercises......Page 515 10 Fundamental Discrete Structures......Page 518 10.1 Ordered pairs......Page 520 10.2 Options......Page 524 10.3 Sets, relations, and functions......Page 526 10.4 Maps......Page 560 10.5 Chapter notes......Page 585 IV Proofs About Algorithms......Page 588 11.1 Defining the algorithm......Page 590 11.2 First correctness properties......Page 596 11.3 Specifying requirements on a function to be defined......Page 601 11.4 Correctness of an optimized binary search algorithm......Page 602 11.5 Summary and looking ahead......Page 603 11.6 Additional exercises......Page 604 12.1 Mathematical background......Page 606 12.2 Strong induction......Page 608 12.3 Properties of half......Page 610 12.4 Properties of odd and even......Page 614 12.5 Properties of power......Page 616 12.6 Properties of fast-power......Page 617 12.7 Tail recursion, a potential optimization......Page 619 12.8 Transforming strong induction into ordinary induction......Page 623 12.9 Measure induction......Page 624 12.11 Additional exercises......Page 626 13.1 Quotient and remainder......Page 630 13.2 The division algorithm......Page 632 13.3 Divisibility......Page 635 13.4 Euclid’s algorithm......Page 643 13.6 Additional exercises......Page 648 13.7 Chapter notes......Page 650 V Proofs at an Abstract Level......Page 652 14.1 Group properties......Page 654 14.2 Theory refinement......Page 658 14.3 Writing proofs at the level of a theory......Page 662 14.4 Abstract proof method conventions......Page 665 14.5 Dynamic evolution of theories......Page 668 14.6 Testing abstract proofs......Page 669 14.7 Group theory refinements......Page 671 14.8 ⋆ Permutations as a group......Page 680 14.9 Ordering properties at an abstract level......Page 691 14.10 Additional exercises......Page 705 15.1 An abstract binary search algorithm......Page 710 15.2 An abstract fast-power algorithm......Page 717 16.1 Axioms and theorems for individual memory locations......Page 730 16.2 Iterators and ranges......Page 736 16.3 Range count algorithm......Page 748 16.4 Range replace algorithm......Page 751 16.5 Range copy algorithm......Page 756 16.6 Range copy-backward algorithm......Page 761 16.7 Adapters: Reverse-iterator and reverse-range......Page 764 16.8 Implementing copy-backward......Page 767 16.9 Random-access iterators......Page 770 16.10 A binary search algorithm......Page 781 16.11 Summary and suggestions for continued study......Page 788 VI Proofs about Programming Languages......Page 792 17.1 Interpreting and compiling numeric expressions......Page 794 17.2 Handling errors explicitly......Page 810 17.3 Chapter notes......Page 824 18.1 A simple imperative language......Page 826 18.2 Semantics of expressions......Page 835 18.3 Semantics of commands......Page 844 18.4 ⋆ Testing the semantics......Page 854 18.5 Some lemmas......Page 860 18.6 Reasoning about the language......Page 871 18.7 Chapter notes......Page 879 Appendices......Page 882 A.1 Syntax......Page 884 A.2 Values......Page 885 A.3 Operational semantics......Page 888 A.4 Pattern matching......Page 902 A.5 Selectors......Page 908 A.6 Prefix syntax......Page 909 B.1 Basics of logic programming......Page 912 B.2 Examples......Page 915 B.3 Implementing a Prolog interpreter......Page 920 B.4 Integration with external Prolog systems......Page 925 B.5 Automating the handling of equations......Page 929 C.1 Representing and reasoning about pizzas......Page 932 C.2 Polymorphic pizzas......Page 941 D Automated Theorem Proving......Page 946 D.1 General automated theorem proving......Page 947 D.2 SMT solving......Page 961 Chapter 2......Page 972 Chapter 3......Page 976 Chapter 4......Page 985 Chapter 5......Page 1037 Chapter 6......Page 1059 Chapter 7......Page 1061 Chapter 8......Page 1062 Chapter 9......Page 1076 Chapter 10......Page 1082 Chapter 11......Page 1099 Chapter 12......Page 1105 Chapter 13......Page 1108 Chapter 14......Page 1110 Chapter 15......Page 1134 Chapter 16......Page 1137 Chapter 17......Page 1153 Chapter 18......Page 1158 References......Page 1186 Glossary......Page 1192 Index......Page 1202