The color coding means:

: all participate
: Doctoral students participate
: next seminar

Please find the abstracts below the schedule and note that some of the slides are made available here, internally.

Date Time Topic Speaker Room
2019 Oct 15 12:45-15:45 The Abstract State Machines Method for High Level System Design and Analysis Egon Börger
(Università di Pisa)
Universität Leipzig
P 501
2019 Oct 22  13:15-16:15 On Dualization in Lattices Given by Their Irreducible Elements or by Implication Bases. Sergei Kuznetsov
(National Research University Higher School of Economics, Moscow)
TU Dresden
APB E005 
2019 Oct 29   moved to January 21    
2019 Nov 12 12:45‑15:45 Temporal Stream-based Specification Language (TeSSLa) Torben Scheffel
(Universität Lübeck)
Universität Leipzig
P 501
Decidability of the HOM Problem in Suitable Weighted Settings Teodora Nasz
2019 Nov 19 13:15-16:15 Temporal constraint satisfaction problems in least fixed point logic Jakub Rydval
(TU Dresden)
TU Dresden
APB E005
Category and Complexity of Spaces in Operator Theory Raj Dahya
(Universität Leipzig)
2019 Nov 26 12:45‑15:45 From Theorem Proving to Cognitive Reasoning Ulrich Furbach
(Universität Koblenz and wizAI GmbH)
Universität Leipzig
P 501
2019 Dec 10 13:15-16:15

Adding Quantitative Taste to FO2 on Words

Bartosz Jan Bednarczyk
(TU Dresden)

TU Dresden
APB E005
Farkas certificates and witnessing subsystems for probabilistic reachability constraints 

Simon Jantsch
(TU Dresden) 

2019 Dec 17 13:15-16:15 Good scientific practice Franz Baader
(TU Dresden)
TU Dresden
APB E005
2020 Jan 7 12:45‑15:45 Geometric complexity theory and fast matrix multiplication Christian Ikenmeyer
(University of Liverpool)
Universität Leipzig
P 501
2020 Jan 14 12:45‑15:45     Universität Leipzig
P 501
2020 Jan 21 13:15-16:15 TBA  Sam van Gool
(IRIF, Université de Paris)
TU Dresden
APB E005
2020 Feb 4 12:45‑15:45     Universität Leipzig
P 501


Egon Börger: The Abstract State Machines Method for High Level System Design and Analysis

We explain the three basic concepts of the Abstract State Machines (ASM) Method for a rigorous development of software intensive systems. The method allows the practitioner to start with an accurate and trustworthy application-domain-centric system model and to link such a `ground model' in a well documented and controllable way through intermediate design steps (called `refinements') to its implementation. The method has been used successfully, under industrial constraints, for the design and analysis of complex hardware/software systems. We highlight some characteristic examples and provide the simple definition of ASMs, starting from scratch. Through its versatility the ASM approach is non-monolithic and integratable at any development level into current software design and analysis environments.

Sergej Kuznetsov: On Dualization in Lattices Given by Their Irreducible Elements or by Implication Bases.

Dualization of a monotone Boolean function can be defined as transformation of the set of minimal 1 values to the set of its maximal 0 values or vice versa. Since dualization is equivalent to many important problems in computer and data sciences, including the famous problem of computing minimal transversals of a hypergraph, the quasi-polynomial dualization algorithm for Boolean lattices proposed by M. Fredman and L. Khachiyan in 1996 was an important breakthrough. It paved the way to generalizations for various classes of structures where dualization in output subexponential time is possible, among them dualization in lattices given by ordered sets of their elements or by products of bounded width lattices, like chains. A well-known fact underlying Formal Concept Analysis (FCA) is that every lattice is determined, up to isomorphism, by the ordered set of its meet (infimum) and join (supremum) irreducible elements. Dualization in the case where a lattice is given by the sets of irreducible elements (i.e., as a concept lattice) has an important application, e.g., it is equivalent to the problem of enumerating minimal hypotheses, a specific type of classifiers in a problem setting about learning from positive and negative examples. We show that dualization for representation of this type is impossible in output polynomial time unless P = NP. However, in an important particular case where the lattice is distributive, a subexponential algorithm can be proposed. We also discuss the complexity of dualization for several partial cases, as well as complexity of dualization when the lattice is given by an implication base. 

Torben Scheffel: Temporal Stream-based Specification Language (TeSSLa)

The Temporal Stream-based Specification Language (TeSSLa) is a specification language developed for the specification of properties over real-time constraints and asynchronous arrival of events on the input streams. A formula of TeSSLa is in the end a function mapping a set of input streams to a set of output streams.
This talk will provide a short introduction to TeSSLa and its application domains at first and then focus on the theoretical results for TeSSLa and various fragments of it regarding other well known formalisms like Turing machines, automata and logics as well as complexity results for different decision problems like equivalence of formulas.

Teodora Nasz: Decidability of the HOM Problem in Suitable Weighted Settings

The HOM problem consists in deciding, given a tree homomorphism H and a regular tree language L represented by a tree automaton, whether H(L) is regular. Guillem Godoy and Omer Giménez proved decidability of this problem in 2010. For this, they introduce and investigate new automata classes and obtain a number of decidability results for these. We discuss their proof as well as ongoing research in generalizing the techniques to suitable semirings.

Jakub Rydval: Temporal constraint satisfaction problems in least fixed point logic

Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in least fixed point logic with counting. 
The border between the two regimes coincides with an important dichotomy in universal algebra. 
For infinite-domain CSPs the situation is more complicated even if the template structure of the CSP is model-theoretically tame. 
We present a complete classification of (infinite-domain) temporal CSPs that can be solved in fixed point logic (with or without counting). 
Our results also show that many naive generalisations of the equivalent conditions in the finite fail to capture expressibility in least fixed point logic already for temporal CSPs.

Raj Dahya: Category and Complexity of Spaces in Operator Theory

Questions arising in other areas of mathematics are sometimes dealt with by appealing to the field set theory. Working over ∞-dimensional, separable Hilbert spaces H, residual results have been achieved for the space, C(H), of contractions under the PW-topology and the space, Hs:=Hom([0,∞),C(H)), of contractive C0-semigroups under the locWOT-topology. Eisner, Mátrai, Serény, et al. raised in various publications 2008–10 the open problems: Are these spaces Baire spaces (weak problem) or even completely metrisable (strong problem)? Positive answers to these questions render the residual results meaningful. To attack this problem, techniques from descriptive set theory (infinite games and hardness/completeness wrt Borel-complexity classes), operator theory (incl. results from dilation) and algebra were utilised. This solves the weak problem and significantly advances our state of knowledge on the strong problem, by reducing a naturally generalised version of it to non-trivial dichotomy. The strong problem is moreover positively solved in the discrete case and for the PW-topology.​

Ulrich Furbach: From Theorem Proving to Cognitive Reasoning

Starting from a depiction of the state of the art in predicate logic theorem proving we address problems which occur if provers are applied in the wild. In particular we discuss how automated reasoning systems can be used for natural language question answering. Our approach to takle common sense reasoning benchmarks within the Corg project ( is presented and we demonstrate how word embeddings can help with the problem of axiom selection. 

Bartosz Bednarczyk: Adding Quantitative Taste to FO2 on Words

The talk will be about the two-variable fragment of First-Order Logic interpreted on words.

Motivation: There are several reasons why logicians could be interested in FO2[<]. First of all, the logic has relatively high expressive power i.e., FO2[<] definable languages belong to the robust fragment of star-free languages. Moreover, it characterizes exactly the Delta_2 alternation fragment of FO[<]. Second, the most interesting computational problems concerning FO2[<] are decidable and have elementary complexity. Lastly, FO2[<] has many connections with temporal logics. It is known that FO2[<] has the same expressive power as UTL[XF, YP] fragment of Unary Temporal Logic and is expressively complete to Propositional Interval Neighbourhood Logic PNLπ+.  

About the talk: We will focus on quantitative extensions of FO2[<]. We will show that the complexity of the satisfiability problem behaves well while extending the logic with threshold-counting or modulo-counting quantifiers. We will prove that, surprisingly, adding just the simple percentage constraints already make the logic undecidable. We will also discuss possible open problems and future research directions in this area.  

The talk will be based on my CSL 2017 && FSTTCS 2017 papers as well as an unpublished paper about the undecidability of FO2[<] with Majority Quantifier, which will appear on arxiv soon. 

Simon Jantsch: Farkas certificates and witnessing subsystems for probabilistic reachability constraints

This talk introduces Farkas certificates for threshold problems on reachability constraints in Markov decision processes (MDP). These certificates are vectors satisfying certain linear inequation systems that we derive by applying variants of Farkas' Lemma to the linear programs characterizing the reachability probabilities in MDP. Farkas' Lemma is a fundamental result in linear algebra that gives, for a system of linear inequalities, a dual system such that one is satisfiable if and only if the other is not. A seemingly independent concept that has been studied in the context of probabilistic reachability is that of a witnessing subsystem. Witnessing subsystems are subsystems that witness a lower-bounded reachability property in the primary system by already having enough probability to reach the target state. We show that a Farkas certificate with K non-zero entries can be translated into a witnessing subsystem with K states, and vice versa. This connection yields new algorithms for the computation of small witnessing subsystems that perform well in practice.

Christian Ikenmeyer: Geometric complexity theory and fast matrix multiplication

The talk gives an introduction to geometric complexity theory, which is an approach towards complexity lower bounds using algebraic geometry and representation theory. We will explain the basic notions, highlight the key challenges, and draw connections to the theory of fast matrix multiplication algorithms.