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.

Abstracts

Nico Potyka: Probabilistic Reasoning with Conflicting Information

Probabilistic logics generalize classical logics by extending the set of classical truth values {0, 1} to the probability interval [0, 1]. In this context, a formula does no longer necessarily evaluate to true or false, but is true with a certain probability. Probability 1 corresponds to classical truth and probability 0 to classical falsity.
In practice, probabilistic knowledge bases often contain conflicting information. For example, empirical probabilities from different statistical surveys should show a similar trend, but are unlikely to be consistent when point probabilities are considered. Similarly, when using subjective probabilities, it is unlikely that two different experts will give completely consistent judgements about the likelihood of events. Since the human brain seems not particularly well suited to grasp probabilities, even probability statements made by a single expert can be inconsistent. However, often these inconsistencies are not substantial and by relaxing probabilistic constraints slightly, we can still derive interesting information that respects the empirical evidence or the experts' intuition "as far as possible".
In this talk, I will first give a quick overview of a simple probabilistic reasoning formalism and some basic approaches that have been considered in order to deal with inconsistencies. Afterwards, we will look at one particular approach to reason over inconsistent probabilistic knowledge bases in more detail. I will explain how to deal with flat and hierarchical inconsistent knowledge bases. Interestingly, the inconsistency-tolerant reasoning problems are often „not significantly harder“ than their classical probabilistic counterparts. They also have some interesting analytical guarantees. For example, if a knowledge base is "almost consistent", the derived probabilities will be "almost classical probabilistic".

Sven Dziadek: Introduction to ω-Algebraic Systems
Or: Have you ever stayed awake at night because you wondered what quemirings are?

The talk will give an introduction to algebraic systems for finite and infinite words and introduce their algebraic structures. Additionally, we give an idea how to construct the Greibach normal form for ω-algebraic systems.

Gustav Grabolle: Variations of nondeterminism using the example of alternating automata
Or: Have you ever stayed awake at night because you wondered what nondeterminism is?

This talk will give an introduction to alternating automata of both kinds: unweighted and weighted.  Our investigation of these formal models will be motivated by by the Question: What is nondeterminism?

Leila Amgoud: Argument-based paraconsistent logics

Handling inconsistency in propositional knowledge bases (KBs) has been studied in AI for a long time. Several two-level logics have been defined: They start with classical propositional logic and define on top of it a non-monotonic logic that infers non-trivial conclusions from an inconsistent KB. There are at least two families of such logics: coherence-based and argument-based logics. The former compute the set of all maximal (for set inclusion) consistent subbases (MCSs) of a KB, and then they apply an inference mechanism for drawing consequences from the MCSs. Argument-based logics follow another process. They justify every candidate consequence of a KB by arguments, generated using the classical consequence relation, then they identify possible conflicts between arguments, evaluate arguments using a formal method, called semantics, and finally keep among the candidate consequences those that are supported by “strong” arguments.  
In this talk, I present three families of argument-based logics that use respectively extension semantics, ranking semantics, and gradual semantics in the evaluation step. I discuss the properties of those logics, and compare them with coherence-based logics.

(cancelled) 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.

Manfred Droste: Random constructions imply symmetry

We will argue for the claim of the title in the areas of algebra, theoretical computer science, and theoretical physics. In algebra, we will consider the random graph. For theoretical computer science, we will give a probabilistic construction of Scott domains used for denotational semantics of programming languages and show that with probability 1 our construction produces a universal homogeneous domain. Finally, we consider causal sets which have been used as basic models for discrete space-time in quantum gravity.

Caterina Viola: Valued Constraint Satisfaction Problems

Introductory talk to the theory of valued constraint satisfaction problems.

Florian Starke: Exploring the Topological Entropy of Formal Languages

We introduce the notions of topological entropy of a formal language and of a topological automaton. We bound the entropy of languages accepted by deterministic ε-free push-down automata with an arbitrary amount of stacks.

Lena Schiffer: Introduction to Combinatory Categorial Grammar
Or: Have you ever stayed awake at night because you wondered what mild context-sensitivity is?

Combinatory Categorial Grammar (CCG) is a mildly context-sensitive grammar formalism that is well-established in computational linguistics.
It has not only a great variety of applications in natural language processing, but is also efficiently parsable. The basis for CCG is provided by a lexicon and a rule system. The lexicon assigns syntactic categories to the symbols of the input and the rule system describes how adjoining categories can be combined to eventually obtain a (binary) derivation tree.
In this presentation, I will give some classical results on the string languages accepted by CCG and some new results on the accepted tree languages.

This talk is based on joint work with Marco Kuhlmann and Andreas Maletti.

Jakob Piribauer: Long-run Satisfaction of Path Properties

We introduce the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold.

This talk is based on joint work with Christel Baier, Nathalie Bertrand, and Ocan Sankur.

Mateus de Oliveira Oliveira: Graph Amalgamation under Logical Constraints

We say that a graph G is an H-amalgamation of graphs G₁ and G₂ if G can be obtained by gluing G₁ and G₂ along isomorphic copies of H.  In the amalgamation recognition problem we are given connected graphs H, G₁, G₂, G and the goal is to determine whether G is an H-amalgamation of G₁ and G₂.
Our main result states that amalgamation recognition can be solved in time 2^{O(Δ·t)·n^O(t)} where n, t, Δ are the number of vertices, the treewidth and the maximum degree of G respectively.

We generalize the techniques employed in our algorithm for H-amalgamation recognition to the setting in which some of the graphs H, G₁, G₂, G are not given explicitly at the input but are instead required to satisfy some topological property expressible in the counting monadic second order logic of graphs (CMSO logic). In this way, when restricting ourselves to graphs of constant treewidth and degree our approach generalizes certain algorithmic decomposition theorems from structural graph theory from the context of clique-sums to the context in which the interface graph H is given at the input.

Frank Drewes: On a Class of Weighted Graph Grammars with Efficient Computation 

The properties of hyperedge-replacement graph grammars parallel those of context-free string grammars in many respects, making them a nice formalism to work with. Unfortunately, the parallels do not extend to the complexity of parsing: even the non-uniform membership problem is NP-complete, i.e., there are NP-complete graph languages that can be generated by hyperedge replacement. To make things worse, most restrictions known to guarantee that the problem is solvable in polynomial time work only in the non-uniform case, because the degree of the polynomial depends on the grammar. While this has been the situation for about three decades now, the question has recently attracted renewed interest, because hyperedge replacement was proposed as a possible formalism for capturing the structure of meaning representations in Natural Language Processing (NLP), where efficient parsing algorithms are of central importance. Another thing required by NLP applications but usually not considered in work on hyperedge replacement is the assignment of weights to generated graphs. In this talk, I will present a class of hyperedge-replacement grammars extended by weights that comes with a parsing algorithm computing the weight of an input graph uniformly in quadratic time.

Deepak Kapur: Conditional Congruence Closure Algorithms for Interpreted Symbols

Algorithms for computing congruence closure and conditional congruence closure of conditional ground equations over uninterpreted and interpreted symbols are presented. The algorithms are based on a recently developed framework for computing (conditional) congruence closure by abstracting non-flat terms by constants as proposed first in Kapur's congruence closure algorithm (RTA97). This framework is general and flexible. It is used also to develop (conditional) congruence closure algorithms for cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combination. It also works for Horn properties including extensionality of function symbols. The concept of a Horn closure of ground equations with uninterpreted as well as interpreted symbols is proposed to decide Horn equations directly.

Jakub Rydval: User-Definable Concrete Domains 

Description logics (DLs) are logical formalisms used in knowledge representation. Concrete domains were introduced to description logics to enable defining concepts using predefined concrete objects and predicates. It is known that allowing general concept inclusions (GCIs) in knowledge bases renders reasoning with some concrete domains undecidable. In this talk, we use standard tools of model theory to study the sufficient condition for decidability of reasoning with concrete domains and GCIs introduced by Lutz and Miličić. In particular, we show that concrete domains based on finitely-bounded homogeneous structures can simultaneously satisfy this condition and have a meaningful application as extensions of description logics.

Frederic Dörband: A comment on the connection between Recognizable Forest Languages and Soluble Groups
Or: How to give a talk with approximately 0 heads-up

The connection is, that I wrote a Master’s Thesis on either of them - about soluble groups in mathematics and about forest languages in computer science. I talk about the individual problems, the formal notions and how the problems were solved.

Recogizable forest languages (RFL) are introduced via an automata model and (a variant of) Kleene’s Theorem is proven. This proof evolves around the observation that RFL are decomposable as a direct product of recognizable tree languages.

Soluble (or: solvable) groups are introduced and Wilson’s Theorem is stated. This theorem states that solubility is FO-characterizable for finite groups where the FO-formula only quantifies a total of 113 elements of the group. Of course, this is surprising - as finite groups can have arbitrary derived length (that is, the number of non-trivial derived subgroups can be arbitrarily large). A proof for Wilson’s Theorem is outlined.

Stefan Göller: Around pushdown automata equivalence and unavoidable patterns

I will survey some old and recent work on the equivalence problem for pushdown automata (language equivalence and bisimulation equivalence). For showing some conceptual lower bound for the equivalence problem of deterministic pushdown automata, I will discuss the asymptotics of the length of longest words that avoid unavoidable patterns. In the second part of my talk I will complement these lower bounds by reporting on recent advances on elementary upper bounds for the equivalence problem of subclasses of deterministic pushdown automata. If time admits, I will conclude with a much too long list of open problems in this area.