Interactive Theorem Proving in Isabelle/HOL

VU3  SS 2026  703315

Introduction

This course provides knowledge about interactive theorem proving with a focus on the Isabelle proof assistant using higher-order logic (HOL). The following topics will be discussed:

  • higher-order logic
  • Isabelle's proof language Isar
  • natural deduction in Isabelle
  • functional programming in Isabelle
  • inductive definitions
  • code generation
  • selection of advanced topics

Literatur

See slides of week 1.

Prerequisites

Knowledge about functional programming and logic.

Content and Schedule

Week Date Topics Slides Sources (rename ".txt" to ".thy") Excercises (rename ".txt" to ".thy")
01 02.03 Organization, Introduction, Higher-Order Logic PDF (x4) Demo.txt Live.txt txt
02 09.03 Pure Framework, Structured Proofs PDF (x4) Demo.txt Live.txt txt
03 16.03 Structured Proofs Continued, Case Analysis and Induction PDF (x4) Demo.txt Live.txt txt
04 23.03 Induction Revisited, Calculational Reasoning, Simplifier PDF (x4) Demo.txt Live.txt txt
05 13.04 Function Definitions Revisited, Manual Termination Proofs, Attributes PDF (x4) Demo.txt Live.txt txt
06 20.04 Projects, Proof Methods, Sledgehammer PDF (x4) Demo.txt Live.txt txt
07 04.05 Inductive Definitions, Rule Inversion and Induction PDF (x4) Demo.txt Live.txt txt
08 11.05 Sets and Lists in Isabelle, Case Study: Binary Search Trees PDF (x4) Demo.txt  
09 18.05 Typedef, Lifting and Transfer      
10 01.06 Code Generation Part 1      
11 08.06 Code Generation Part 2      
12 15.06 Sessions, Document Preparation, Type Classes      
13 22.06 Further Topics, Master Projects      

 

Evaluation

  • There are weekly exercises that count 50 % of the overall grade and a project that counts another 50 %.
  • Solved exercises must be marked and uploaded in OLAT. The deadline is Monday, 6 am before the lecture. Solutions will be made available in OLAT.
  • The projects are available as PDF and after the assignment also as Isabelle theories.
  • The projects will be presented on April 20, and then also the project distribution will be conducted. Each project is designed for 1, 2 or 3 persons.
  • The deadline for handing in completed projects is August 1st.
Evaluation of projects is based on
  • number and significance of remaining sorrys
  • readability and clarity of submitted Isabelle theory
  • successful document generation of submitted Isabelle theory
  • personal interview on each project, where project related questions will be asked
Project assignment
  • Congruence Closure: AKo, AP, AvU
  • Propositional Logic: PD, AM
  • Tseitin Transformation: MC, JM
  • Register Machine: AKu
  • BigNat: SD
  • Euclidean Inductive: LS