Research Group Leaders




Jonathan Gärtner
Johanna Meerjanssen

Former Students

Fajar Haifani (Ph.D. 2023): On a Notion of Abduction and Relevance for First-Order Logic Clause Sets
Mathias Fleury (Ph.D. 2020): Formalization of Logical Calculi in Isabelle/HOL
Martin Bromberger (Ph.D. 2019): Decision Procedures for Linear Arithmetic
Marco Voigt (Ph.D. 2019): Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
Andreas Teucke (Ph.D. 2018): An Approximation and Refinement Approach to First-Order Automated Reasoning
Ching Hoo Tang (Ph.D. 2017): Logics for Rule-Based Configuration Systems
Daniel Wand (Ph.D. 2017): Superposition: Types and Induction
Marek Kosta (Ph.D. 2016): New Concepts for Real Quantifier Elimination by Virtual Substitution
Noran Azmy (Ph.D. 2016): A Machine–Checked Proof of Correctness of Pastry
Martin Suda (Ph.D. 2015): Resolution-based methods for linear temporal reasoning
Manuel Lamotte-Schubert (Ph.D. 2015): Automatic Authorization Analysis
Willem Hagemann (Ph.D. 2015): Symbolic Orthogonal Projections: A New Polyhedral Presentation for Reachability Analysis of Hybrid Systems
Arnaud Fietzke (Ph.D. 2014): Labelled Superposition
Tianxiang Lu (Ph.D. 2013): Formal Verification of the Pastry Protocol
Evgeny Kruglov (Ph.D. 2013): Superposition Modulo Theory
Patrick Wischnewski (Ph.D. 2012): Efficient Reasoning Procedures for Complex First-Order Theories
Carsten Ihlemann (Ph.D. 2010): Reasoning in Combinations of Theories
Matthias Horbach (Ph.D. 2010): Saturation-Based Decision Procedures for Fixed Domain and Minimal Model Validity
Swen Jacobs (Ph.D. 2010): Hierarchic Decision Procedures for Verification
Thomas Hillenbrand (Ph.D. 2009): Superposition and Decision Procedures Back and Forth