Description

The course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade provers, teaches the theoretical backround to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The course is intended to bring master students into contact with current research topics in the field of theorem proving and automated deduction, and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification.

The theorem prover Isabelle/HOL will be used in the course. Topics include higher-order logic, natural deduction, lambda calculus, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs and proofs about programs.

Prerequisites

Must have previous experience with logic and functional programming.

Content

• Intro & motivation
• Foundations & principles
  • Lambda Calculus
  • Higher-Order Logic, natural deduction
  • Term rewriting
• Proof & specification techniques
  • Datatypes, recursion, induction
  • Inductively defined sets, rule induction
  • Calculational reasoning, mathematics style proofs
  • Hoare logic, proofs about programs

Literature

The tutorial on Isabelle/HOL

Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer, 2002. ISBN: 3-540-43376-7.

is a comprehensive introduction to Isabelle/HOL. It does not cover the new ISAR proof language that will be used in the course, though. If you do not want to buy it, you may (legally!) download it here.