Have you ever wanted or needed to prove a property about a formal system but did not know where to start or what techniques to use? Have you ever had trouble sleeping, worrying whether you made a mistake in a paper you just submitted to a conference? If so then this course is for you. The course is a hands-on introduction to theorem proving using the Isabelle proof assistant and the Isar proof language (``Isar'' stands for Intelligible Semi-Automated Reasoning). The course will cover reasoning about inductive datatypes, recursive functions, and sets using propositional, predicate, and higher-order logic (HOL). The course will cover common proof techniques including a cornucopia of induction methods. Last but not least, this course will cover practical issues such as how to ``debug'' your proofs, techniques for structuring large proofs, how to make the best use of Isabelle's decision procedures, and how to get Isabelle to typeset your definitions and proofs in LaTeX. The course has no explicit prerequisites, but a basic understanding of logic is helpful, as is some exposure to functional programming.
I recommend that you bring a laptop computer to class and have a working installation of Isabelle 2005 (see below).
When using Proof General (an extension of xemacs for interactive Isabelle development), I typically turn on support for x-symbol (menu Proof-General -> Options) and for multiple windows (menu Proof-General -> Options -> Display).
Note for Mac-on-Intel users. Isabelle normally uses polyml for its underlying ML implementation, but polyml has not yet been ported to the Intel macs. Instead you can use SML of NJ. Here's some links to help: