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:4515: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:1516: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 Streambased 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:1516: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:1516:15 
Bartosz Jan Bednarczyk 
TU Dresden APB E005 

Farkas certificates and witnessing subsystems for probabilistic reachability constraints 
Simon Jantsch 

2019 Dec 17  13:1516: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:1516: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 
Abstracts
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 applicationdomaincentric 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 nonmonolithic 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 quasipolynomial 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 wellknown 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 Streambased Specification Language (TeSSLa)
The Temporal Streambased Specification Language (TeSSLa) is a specification language developed for the specification of properties over realtime 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
Raj Dahya: Category and Complexity of Spaces in Operator Theory
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 (http://corg.hsharz.de) 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 twovariable fragment of FirstOrder 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 starfree 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 thresholdcounting or modulocounting 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 lowerbounded reachability property in the primary system by already having enough probability to reach the target state. We show that a Farkas certificate with K nonzero 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.