Prof. Dr. Thomas Zeume

Logic and Formal Verification


Tel.: +49(0) 234 32-19609
Room: IB 3/129

Consultation hours

By arrangement



since October 2020

April 2020 – October 2020


2004 – 2009

Professorship for Logic and Formal Verification
Faculty of Mathematics & Center of Computer Science, RUB
Assistant Professorship for Logic and Formal Verification
Faculty of Mathematics & Center of Computer Science, RUB
Doctorate in Theoretical Computer Science
TU Dortmund
Computer Science Studies
Leibniz-Universität Hannover

  • Logic in computer science
  • Formal verification
  • Complexity theory
  • Automata theory

Research interests

My research interests lie at the interface of mathematics and computer science. My research focuses on the application of logical and complexity-theoretic methods to computer science scenarios, in particular database theory and verification.

Querying dynamic databases

Extracting information from vast amounts of data that are frequently updated is a major challenge in many disciplines. Dynamic complexity theory studies the theoretical foundations of logical query languages for databases that are subject to frequent changes. One of the main goals in this area is to develop a theory for classifying queries in terms of the amount of resources needed to evaluate them dynamically.

My research investigates (a) methods for determining the set of resources needed to sustain queries in this dynamic context, and (b) the structure of small dynamic complexity classes and their relationship to traditional static complexity classes.

A good start to the area:

Logic for Specification and Verification

Automated verification of software and hardware is an important task. Often intended properties of a system are specified by logical formalisms that navigate along traces of the system. Similar formalisms are the basis for query languages for extracting information from XML documents and graph databases.

In my research, I explore logical systems with respect to their applicability for such tasks. I contributed to the design of a navigational logic, DataLTL, that allows for specifying complex properties of systems with many processes, and whose basic reasoning tasks remain decidable. For another basic specification language, the two-variable fragment of predicate logic, we study the complexity of reasoning tasks for many variants and were able to give a classification of their computational complexity

Selected papers

A web-based system for learning logic

A typical application of logic in computer science is to model a real-world scenario, formulate formulas expressing knowledge about the scenario, and derive new knowledge through logical reasoning. While there is no shortage of software for logic, a closer look reveals that there is almost no current intuitive software system to support student learning for such basic instructional goals.

Our goal is to build such an interactive, web-based system that supports tasks for traditional logic (propositional logic, modal logic, and predicate logic), as well as more domain-specific logic used for verification and database query tasks.

Try it: Logic Web Tutorial

Introduction to the System: 


Here you can find an up-to-date list of my publications.

Journal Articles
  • Thomas Zeume. Small Dynamic Complexity Classes: An Investigation into Dynamic Descriptive Complexity, volume 10110 of Lecture Notes in Computer Science. Springer, 2017.
  • Johannes Albrecht, Carsten Brenner, Bilal Gökce, Pascal Malkemper, Jochen Niemeyer, and Thomas Zeume. I Love to Share Knowledge: A personal perspective on academic teaching. Universität Duisburg-Essen, 2017. ISBN: 978-3-940402-09-7.

Conference papers
  • (Poster) Gaetano Geck, Artur Ljulin, Jonas Haldimann, Johannes May, Jonas Schmidt, Marko Schmellenkamp, Daniel Sonnabend, Felix Tschirbs, Fabian Vehlken, Thomas Zeume: Teaching Logic with Iltis: an Interactive, Web-Based System. ITiCSE 2019: 307
  • Thomas Schwentick, Thomas Zeume: Dynamic complexity: recent updates. SIGLOG News 3(2): 30-52 (2016)
  • PhD thesis: Small Dynamic Complexity Classes. 2015. Reviewers: Erich Grädel, Thomas Schwentick
  • Diploma thesis: Small Dynamic Complexity Classes. 2009. Examiners: Jarkko Kari, Heribert Vollmer.