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

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.

Table of Contents

Part I Introduction
Chapter 1 An Overview Of Fundamental Proof Methods
Chapter 2 Introduction To Athena

Part II Fundamental Proof Methods
Chapter 3 Proving Equalities
Chapter 4 Sentential Logic
Chapter 5 First-Order Logic
Chapter 6 Implication Chaining

Part III Proofs About Fundamental Datatypes
Chapter 7 Organizing Theory Development With Athena Modules
Chapter 8 Natural Number Orderings
Chapter 9 Integer Representations And Proof Mappings
Chapter 10 Fundamental Discrete Structures
Part IV Proofs About Algorithms
Chapter 11 A Binary Search Algorithm
Chapter 12 A Fast Exponentiation Algorithm
Chapter 13 Euclid’S Algorithm For Greatest Common Divisors

Part V Proofs At An Abstract Level
Chapter 14 Abstract Structures
Chapter 15 Abstract Algorithms
Chapter 16 Algorithms On Memory Abstractions

Part VI Proofs About Programming Languages
Chapter 17 A Correctness Proof For A Toy Compiler
Chapter 18 A Simple Imperative Programming Language

Appendix A Athena Reference
Appendix B Logic Programming And Prolog
Appendix C Pizza, Recursion, And Induction
Appendix D Automated Theorem Proving
Appendix E Solutions To Selected Exercises