by Arkoudas, Musser
ISBN: 9780262342490  Copyright 2017
TabsExpand/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 Metaidentifiers (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 Topdown 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 FirstOrder 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 firstorder logic (pg. 353)  
5.6 Firstorder 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 chainlast (pg. 411)  
6.5 Backward chains and chainfirst (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 fastpower (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 fastpower 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 copybackward algorithm (pg. 734)  
16.7 Adapters: Reverseiterator and reverserange (pg. 737)  
16.8 Implementing copybackward (pg. 740)  
16.9 Randomaccess 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 is a Senior Research Scientist and Software Architect at Bloomberg.
David Musser is Professor Emeritus of Computer Science at Rensselaer Polytechnic Institute.
Instructors  

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.
Device Compatibility Features
