Courses
Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic (ESSAI'26, Summer School, Vienna, Austria, Joint Lecturer with Hannes Straß)
Details for the course can be found at the following link: [Course Details]
Proof Theory and Sequent Systems (TUD, Summer Semester 2026)
Details for the course can be found at the following link: [Course Details]
The course script can be downloaded at the following link: [Script]
Proof Theory and Sequent Systems (TUD, Winter Semester 2025)
Details for the course can be found at the following link: [Course Details]
The course script can be downloaded at the following link: [Script]
Proof Theory and Sequent Systems (TUD, Summer Semester 2024)
Details for the course can be found at the following link: [Course Details]
The course script can be downloaded at the following link: [Script]
Templates
Master's Thesis Template (Fakultät Informatik, Technische Universität Dresden) [Download]
Project Template (Technische Universität Dresden) [Download]
Supervision and Assessment
Master's Thesis Supervision:
MSc Thesis (TUD, Summer Semester 2026)
Title: TBD [Thesis]
Student: Youssef Hamdy
Abstract: TBD
MSc Thesis (TUD, Summer Semester 2026)
Title: TBD [Thesis]
Student: Omar Y. A. A. Taher
Abstract: TBD
Master's Project Supervision:
Research Project (TUD, Summer Semester 2025)
Title: Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents [Technical Report]
Student: Omar Y. A. A. Taher
Abstract: This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
Thesis Examination/Review:
MSc Thesis (TUD, Summer Semester 2026)
Title: Formalizing the Core Chase in Lean [Thesis]
Student: Henrik Tscherny
Abstract: This thesis formally verifies the foundational result that the core chase algorithm—a refined variant of the chase used to generate models of knowledge bases for conjunctive query answering—always terminates with a finite, universal model whenever such a model exists. The verification provides rigorous, machine-checkable proofs of this result.