- 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.
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.
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...
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...
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.
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.
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...
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...
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...
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,...
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)...
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...
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,...
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.
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...