29 July 2025: Aart Middeldorp receives two prestigious research awards

In this year at the CADE conference, Aart Middeldorp was awarded with both the Herbrand Award and the in combination with Nao Hirokawa, he also receiv

10 November 2022: CL congratulates Thomas Oberroither

Thomas Oberroither is the winner of the Best Bachelor Thesis award of the academic year 2021/2022. He was awarded at the inday students for his thesis

18 August 2024: 4 year PhD position available

A 4 year PhD position is available. Click here for details.

29 August, 2023: Johannes Niederhauser completes his master studies

Johannes Niederhauser successfully defends his master thesis, entitled “Left-linear Completion with AC Axioms”. Congratulations. We are delighted that

ISR 2026

This site provides supporting material for the lecture Tree Automata Techniques in Term Rewriting at ISR 2026.

Slides

Course material

 

Master Program - 703319 - Research Seminar in Logic and Learning: CL/TCS

Master Program - Research Seminar in Logic and Learning: CL/TCS

SE2  SS 2026  703319

News

 Overview

Introduction

In the seminar we study current topics relevant to logic and learning. For master students interested in these topics, the seminar provides an ideal preparation for a master project in the Computation Logic and Theoretical Computer Science research groups.

Supervisors

  Room Consultation Hours
Manuel Eberl 3M03 Thursday, 10:30  - 11:30
Aart Middeldorp 3M07 Monday, 12:00 – 13:30
Georg Moser 1N05 Wednesday, 12:00 – 14:00
Arnab Roy 3M12 by arrangement
René Thiemann 3M09 Tuesday, 10:15 – 11:15

Time & Place

The seminar takes place on Wednesdays, 8:30 - 10:00 in 3W04. In the slot on March 4th, seminar topics will be presented, distributed and the scheduling for the talks will happen.

Grading

For master students the grade is based on presentation, seminar report, and active participation. For PhD students, presentation and very active participation is taken into account.

Master Program - 703315 - Interactive Theorem Proving in Isabelle/HOL

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