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

Time & Place

The seminar takes place on Wednesdays, 8:30 - 10:00 in 3W04. In the slot on March 4^th, 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.

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

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 1^st.

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

Master Program - Constraint Solving

VO2 + PS2  SS 2026  703304 + 703305

Overview

Lecturer

Time and Place

The lecture (VO) starts on March 4^th, the first exercise session (PS) is on March 10^th.

Content

The elective module Constraint Solving provides an introduction into the theory and practice of constraint solving. The following topics will be discussed:

• propositional logic (SAT and Max-SAT)
• Boolean combination of constraints, satisfiability modulo theories (SMT)
• constraints about equality logic and uninterpreted functions (EUF)
• linear arithmetic constraints (LIA and LRA)
• constraints involving arrays
• constraints using quantifiers (QBF)

All material (slides, homework sheets, solutions, lecture recordings) are available on the OLAT sites of the lecture and proseminar.

Exam

The first exam will be on June 24. It will be closed book.
You can find old exams on this website of a previous iteration of this course.

Literature

The course is partly based on the following books:

• Daniel Kroenig and Ofer Strichman
  Decision Procedures — An Algorithmic Point of View (second edition).
  Springer, 2016
• Aaron Bradley and Zohar Manna
  The Calculus of Computation — Decision Procedures with Applications to Verification.
  Springer, 2007