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:

• Thomas Schwentick, Thomas Zeume: Dynamic complexity: recent updates. SIGLOG News 3(2): 30-52 (2016)
• Thomas Zeume. Small Dynamic Complexity Classes. PhD thesis. 2015.
• Slides: Thomas Zeume. An Update on Dynamic Complexity. ICDT 2018
  
  

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

• Thomas Schwentick and Thomas Zeume: Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science. 2012.
• Thomas Zeume and Frederik Harwath: Order-Invariance of Two-Variable Logic is Decidable. LICS 2016. (Extended version)
• Ahmet Kara, Thomas Schwentick, and Thomas Zeume: Temporal Logics on Words with Multiple Data Values. FSTTCS 2010: 481-492 (Extended version)
  
  

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: 

• Gaetano Geck, Artur Ljulin, Sebastian Peter, Jonas Schmidt, Fabian Vehlken, Thomas Zeume. Introduction to Iltis: An Interactive, Web-Based System for Teaching Logic. To be presented at ITiCSE 2018.