ISR 2008

3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track B – A Practical Introduction to Theorem Proving with Isabelle


Tobias Nipkow


Isabelle/HOL is an interactive theorem prover for HOL, a popular version of higher-order logic. The purpose of this tutorial is to familiarize students, researchers and practitioners with the basics of specification and proof in Isabelle/HOL. The course combines traditional lectures, on-line demos, and practical exercises for the participants. At the end of the course participants should be able to formalize functional programs and set-theoretic system models and prove (with Isabelle’s help) simple properties about them. The following topics are covered: