Logic and Formal Verification
This home page was used to support the second week of the Carnegie Mellon Summer School in Logic and Formal Epistemology in the summer of 2009. Due to copyright restrictions, some of the materials are in a password protected directory.
Background on logic and axiomatic reasoning
For the session on formal verification, you may wish to review the basics of symbolic logic. Here are some good references:
- Barwise, Jon, and John Etchemendy, Language, Proof, and Logic. Amazon: html.
- Enderton, Herbert, A Mathematical Introduction to Logic. Amazon: html.
- Goldfarb, Warren, Deductive Logic. Amazon: html.
The following is a good introduction to axiomatic reasoning in mathematics:
- Stewart, Ian, and David Tall, The Foundations of Mathematics. Amazon: html.
Background on the Isabelle proof assistant
We will experiment with an interactive proof system called Isabelle.
- The Isabelle home page: html.
- The Isabelle documentation page: html.
- See especially the tutorial: pdf.
The Linux installation of Isabelle is quick and easy.
We will use "Isabelle/HOL," an instantiation of higher-order logic. You can browse the library of theorems and definitions here:
- The Isabelle/HOL library: html.
I will do a good deal of "borrowing" from the course material page: html. See especially:
- The Isabelle/HOL exercises: html.
- The interactive course by Brucker et al.: html. Slides: html. Exercises: html.
There are sketchy lecture notes for the first three topics: pdf. And here is Henry Towsner's handy Isabelle "cheat sheet": pdf.
- See Sections 5.1-5.7 of the tutorial.
- See also the relevant lectures and exercises in the Brucker et al. course: pdf, pdf.
- An exercise involving the rules of propositional logic: pdf.
- An exercise on eliminationg connectives: pdf.
First-order logic with equality
- See Section 5.9 of the tutorial.
- See also the relevant lectures and exercises in the Brucker et al. course: pdf, pdf, pdf.
- An exercise using the quantifiers: pdf.
- An exercise, the "Rich Grandfather" riddle: pdf.
Induction and recursion on the natural numbers
- An excerpt from Stewart and Tall on the natural numbers: pdf.
- See Sections 2.5 and 3.5 of the tutorial.
- See also the relevant lecturesand exercises from the Brucker et al. course: pdf.
- An exercise involving powers and sums: pdf.
- An exercise involving "magical methods": pdf.
Beyond the natural numbers
- Higher-order logic, simple type theory and set theory: see the tutorial, and Brucker et al. lectures.
- Inductively defined sets: see the tutorial, and Brucker et al. lectures.
Interlude: formal verification and understanding
For a short, sweeping overview of the philosophy of mathematics, see
- Avigad, "Philosophy of Mathematics": pdf.
For a look a discussion of some new philosophical issues related to the use of computers in mathematics, see:
- Avigad, "Mathematical Method and Proof": pdf.
- Avigad, "Computers in mathematical inquiry": pdf.
- Avigad, "Understanding proofs": pdf.
The last of these adopts a Wittgensteinian perspective on the nature of mathematical understanding. See the following excerpt from the Philosophical Investigations:
- Wittgenstein on rule following: pdf.
Interlude: decision procedures
- A graduate level seminar on decision procedures: html.
- A lecture by Yiannis Moschovakis, "Solving Equations in Algebra and Arithmetic," in the 2008 summer school: pdf.
- A lecture for the 2006 summer school: pdf.
Interlude: an analysis of Euclidean diagrammatic reasoning
- A talk for philosophers and historians of mathematics: pdf.
- A talk for computer scientists: pdf.
Some thoerem provers
Some formal verification links
- References for proof theory: html.
- Some fun logic puzzles from Smullyan, The Lady or the Tiger: pdf.