3rd International School on Rewriting
21 – 26 July 2008, Obergurgl, Austria
Program – Track B – A Practical Introduction to Theorem Proving with Isabelle
Lecturer
Tobias NipkowIntroduction
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:
- datatypes and recursive functions,
- proof by structural induction and by simplification,
- proofs in propositional logic and predicate logic,
- set theory and inductively defined sets,
- a language of readable proofs.