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

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