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:

The following is a good introduction to axiomatic reasoning in mathematics:

Background on the Isabelle proof assistant

We will experiment with an interactive proof system called Isabelle.

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:

I will do a good deal of "borrowing" from the course material page: html. See especially:

Lecture notes

There are sketchy lecture notes for the first three topics: pdf. And here is Henry Towsner's handy Isabelle "cheat sheet": pdf.

Propositional logic

First-order logic with equality

Induction and recursion on the natural numbers

Beyond the natural numbers

Interlude: formal verification and understanding

For a short, sweeping overview of the philosophy of mathematics, see

For a look a discussion of some new philosophical issues related to the use of computers in mathematics, see:

The last of these adopts a Wittgensteinian perspective on the nature of mathematical understanding. See the following excerpt from the Philosophical Investigations:

Interlude: decision procedures

Interlude: an analysis of Euclidean diagrammatic reasoning

Some thoerem provers

Some formal verification links