Thomas Zeume

ORCID: 0000-0002-5186-7507
Publications
Citations
Views
---
Saved
---
About
Contact & Profiles
Research Areas
  • Logic, programming, and type systems
  • semigroups and automata theory
  • Logic, Reasoning, and Knowledge
  • Advanced Database Systems and Queries
  • Formal Methods in Verification
  • Computability, Logic, AI Algorithms
  • Complexity and Algorithms in Graphs
  • Algorithms and Data Compression
  • Data Management and Algorithms
  • Intelligent Tutoring Systems and Adaptive Learning
  • Advanced Algebra and Logic
  • Advanced Graph Theory Research
  • Semantic Web and Ontologies
  • Innovative Teaching and Learning Methods
  • Teaching and Learning Programming
  • Machine Learning and Algorithms
  • Graph Theory and Algorithms
  • Cellular Automata and Applications
  • Distributed systems and fault tolerance
  • Optimization and Search Problems
  • Experimental Learning in Engineering
  • Parallel Computing and Optimization Techniques
  • Online Learning and Analytics
  • Online and Blended Learning
  • Natural Language Processing Techniques

Ruhr University Bochum
2019-2025

University of Zurich
2021

TU Dortmund University
2010-2020

Leibniz University Hannover
2009-2010

It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor linear order relation and some further unary relations EXPSPACE-complete. Actually, EXPSPACE-completeness already holds do not include relation. As a special case, EXPSPACE upper bound applies to two orders. A consequence of data words on positions decidable in EXPSPACE. complementing result, it as well relations, undecidable.

10.2168/lmcs-8(1:15)2012 article EN cc-by Logical Methods in Computer Science 2012-03-02

It is shown that order-invariance of two-variable first-logic decidable in the finite. This an immediate consequence a decision procedure obtained for finite satisfiability problem existential second-order logic with two first-order variables (ESO2) on structures linear orders and one induced successor. We also show successors order. In both cases, so far only decidability monadic ESO2 has been known. addition, order its successor relation to be non-deterministic exponential time.

10.1145/2933575.2933594 article EN 2016-07-05

In this report, we survey the existing scholarship in STEM higher education regarding what motivates, encourages, and inhibits educators' decisions to adopt teaching innovations. After reviewing common theoretical foundations considerations for adoption dissemination studies, identify challenges encouraging among educators education. When possible, provide evidence-based recommendations from literature on how overcome these challenges. We then consider relevance of general other disciplines...

10.1145/3293881.3295785 article EN 2018-07-02

This paper continues the study of two-variable fragment first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from set \Sigma x D where a alphabet an domain. These naturally represented as labelled sets linear order <=_l total preorder <=_p. We introduce automata, automaton model for words. An composition...

10.4230/lipics.csl.2013.484 article EN Computer Science Logic 2013-01-01

Patnaik and Immerman introduced the dynamic complexity class DynFO of database queries that can be maintained by first-order programs with help auxiliary relations under insertions deletions edges. This article confirms their conjecture reachability query is in DynFO. As a byproduct, it shown rank matrix small values It further (size the) maximum matching graph non-uniform DynFO, an extension initialisation relations.

10.1145/3212685 article EN Journal of the ACM 2018-08-29

In many data management scenarios the is subject to frequent modifications, and it often essential react those changes quickly. When a train canceled on short notice, travelers need find alternative connections as fast possible. web server temporarily not available, packages have be rerouted immediately.

10.1145/2948896.2948899 article EN ACM SIGLOG News 2016-05-31

The paper proposes and studies temporal logics for attributed words, that is, data words with a (finite) set of (attribute,value)-pairs at each position. It considers basic logic which is semantical fragment the $LTL^\downarrow_1$ Demri Lazic operators navigation into future past. By reduction to emptiness problem automata it shown this decidable. Whereas only allows positions where fixed value occurs, extensions are studied also allow different values. Besides some undecidable results...

10.48550/arxiv.1010.1139 preprint EN other-oa arXiv (Cornell University) 2010-01-01

10.1016/j.ic.2014.09.011 article EN publisher-specific-oa Information and Computation 2014-10-04

We are interested in the following validation problem for computational reductions: algorithmic problems $P$ and $P^\star$, is a given candidate reduction indeed from to $P^\star$? Unsurprisingly, this undecidable even very restricted classes of reductions. This leads question: Is there natural, expressive class reductions which can be attacked algorithmically? answer question positively by introducing an easy-to-use graphical specification mechanism reductions, called cookbook show that...

10.4230/lipics.mfcs.2024.56 preprint EN arXiv (Cornell University) 2024-08-26

The paper proposes and studies temporal logics for attributed words, that is, data words with a (finite) set of (attribute,value)-pairs at each position. It considers basic logic which is semantical fragment the $\LTL^\downarrow_1$ Demri Lazic operators navigation into future past. By reduction to emptiness problem automata it shown this decidable. Whereas only allows positions where fixed value occurs, extensions are studied also allow different values. Besides some undecidable results...

10.4230/lipics.fsttcs.2010.481 article EN 2010-10-01

Graph databases in many applications - semantic web, transport or biological networks among others are not only large, but also frequently modified. Evaluating graph queries this dynamic context is a challenging task, as those often combine first-order and navigational features. Motivated by recent results on maintaining reachability, we study the evaluation of traditional query languages for graphs descriptive complexity framework. Our focus regular path queries, extensions thereof,...

10.4230/lipics.icdt.2016.14 article EN International Conference on Database Theory 2016-01-01

10.1016/j.ic.2017.04.005 article EN Information and Computation 2017-04-27

Logic is a foundation for many modern areas of computer science. In artificial intelligence, as basis database query languages, well in formal software and hardware verification --- modelling scenarios using logical formalisms inferring new knowledge are important skills going-to-be scientists. The Iltis project aims at providing web-based, interactive system that supports teaching methods. particular the shall (a) support to learn model infer propositional logic, modal logic first-order (b)...

10.1145/3197091.3197095 preprint EN 2018-06-20

In the setting of DynFO, dynamic programs update stored result a query whenever underlying data changes. This is expressed in terms first-order logic. We introduce strategy for constructing that utilises periodic computation auxiliary from scratch and ability to maintain limited number change steps. show if some program can log n steps after an AC$^1$-computable initialisation, it be maintained by as well, i.e., DynFO. As application, shown decision optimisation problems defined monadic...

10.23638/lmcs-15(2:12)2019 article EN cc-by Logical Methods in Computer Science 2019-05-08

In the setting of dynamic complexity, goal a program is to maintain result fixed query for an input database that subject changes, possibly using additional auxiliary relations. other words, updates materialized view whenever base relation changed. The update and relations specified first-order logic or, equivalently, relational algebra. original framework by Patnaik Immerman only considers changes insert or delete single tuples. This article extends definable , also queries on database,...

10.1145/3241040 article EN ACM Transactions on Database Systems 2018-09-30

How can the result of a query be updated after changing database? This is fundamental task for database management systems which ideally takes previously computed information into account. In dynamic complexity theory, it studied from theoretical perspective where updates are specified by rules written in first-order logic. this article we sketch recent techniques and results theory with focus on reachability query.

10.1145/3442322.3442325 article EN ACM SIGMOD Record 2020-12-09

Recently it was shown that the transitive closure of a directed graph can be updated using first-order formulas after insertions and deletions single edges in dynamic descriptive complexity framework by Dong, Su, Topor, Patnaik Immerman. In other words, Reachability is DynFO. In this article we extend to changes multiple at time, study Distance queries under these changes. We show former problem maintained DynFO(+, x) affecting O({log n}/{log log n}) nodes, for graphs with n nodes. If update...

10.4230/lipics.icalp.2018.120 article EN International Colloquium on Automata, Languages and Programming 2018-01-01
Coming Soon ...