The ninth edition of the QuantLA workshop is held as an online event from October 6 to October 8, 2021. Each session consists of several talks, given by current scholarship holders or students associated with the research training group, hosted on the Zoom platform. All of the events, with the exception of PIs meetings, are accessible at the following link. Complete credentials are provided via the internal mailing lists.

Program outline

Wednesday, October 6

Thursday, October 7

Friday, October 8

Program

Wednesday, October 6

Session 1: Description Logics I

Filippo De Bortoli: Description Logics that Count in Practice

The description logic ALCSCC extends the knowledge representation language ALC with numerical constraints, given by linear inequalities over cardinalities of role-successor sets, acting on a local level. ALCSCC ERCBoxes, which restrict cardinalities of ALCSCC concepts in an interpretation, are positive Boolean combinations of systems of linear inequalities Ax <= b, with b >= 0. Finite consistency of an ALCSCC ERCBox, i.e. checking if it has a finite model, is an ExpTime-complete decision problem (Baader, Bednarczyk & Rudolph, 2020). The upper bound proof uses an algorithm based on type elimination, which runs in best-case exponential time in the size of the ERCBox.
Using these counting formalisms, we can express other interesting constructors, such as probabilistic conditionals over interpretations (Peñaloza & Potyka, 2017) and perceptron operators (Galliani, Kutz & Troquard, 2021). To facilitate their adoption in building real-world ontologies, it is thus crucial to design efficient decision procedures for finite consistency of ALCSCC ERCBoxes. We present an algorithm that decides the finite consistency of a conjunctive ERCBox over concepts in a fragment of ALCSCC. Our approach is based on the principle of column generation and avoids the best-case behavior of the type elimination algorithm. We first illustrate how it operates on ALCSCC concept descriptions. Then, we show how to extend it to account for the interplay between numerical constraints on the local and the global level.

Willi Hieke: Counter Model Transformation for Explaining Non-Subsumption in EL

When subsumption relationships unexpectedly fail to be detected by a description logic reasoner, the cause for this “non-entailment” need not be evident. In this case, succinct and automatically generated explanations are helpful. Reasoners for the description logic EL compute the canonical model of a TBox in order to perform subsumption tests. We devise parts of such models as relevant parts for explanation and propose an approach based on graph transductions to extract such relevant parts from canonical models

Christian Alrabbaa: Explications of DL Reasoning - Exploring the Whys and Hows

Decisions made by complex systems can be hard to understand, and a system having the capability of explaining its decisions is a desired one. Moreover, if a decision leads to an undesired behavior, the need to provide an explanation becomes more important. In this talk, I address the issue of explaining the results of Description Logic reasoning, in particular, how a DL knowledge base system can provide explanations for both logical entailments as well as non-entailments. Explaining non-entailments can be done by means of countermodels. I present our evaluation results of a tool we implemented for extracting different relevant parts of countermodels for the DL EL, which allows to provide concise explanations. I also discuss how formal proofs can be used to explain entailments. I go through different examples of proof measures and introduce two classes that generalize those measures. In order to provide concise explanations of entailments, I present our complexity results for computing optimal proofs. In the last part of the presentation, I talk about proofs in practice, our implementation for interactive proofs, and how it was used in a user study for exploring the impact of different proof representations on the understanding of proofs.

Thursday, October 7

Session 2: Weighted Automata I

Gustav Grabolle: The search for MSO characterizations of weighted universal automata, weighted leveled automata, and weighted alternating automata

Sadly, the well known equivalence between recognizable languages and MSO logic does not translate to the weighted setting. While we may translate any weighted automaton into a weighted MSO formula, the converse does not hold true. Simply by the use of the product quantifier for sets, weighted MSO logic can define series, that grow doubly exponential in the length of the input. This is impossible to achieve with a weighted automaton. Alternating weighted automata on the other hand posses the power of multiplying several runs on a given input. By this, they too, can define series with doubly exponential growth. Are weighted alternating automata enough to rival the expressive power of weighted MSO?
We approach this question, by giving MSO characterizations for two subclasses of weighted alternating automata. First, we search for a fragment of weighted MSO that is as expressive as weighted universal automata. We prove, that weighted universal automata are not closed under sums, but under multiplicative inverses of homomorphisms. By these results, we identify a fitting fragment of weighted MSO and prove that it characterizes weighted universal automata. Next, we define a MSO fragment mirroring the hierarchical structure of leveled automata and show their equivalence. Finally, we compare the full class of weighted alternating automata, to the full power of weighed MSO logic.

Kevin Stier: Disambiguation of Weighted Tree Automata

We extend the disambiguation construction presented by Mohri and Riley in 2017 in two ways. First we change the underlying structure of their automata from words to trees, and second we show that these results hold not only for the tropical semiring but also the arctic one.

Session 3: Weighted Automata II + Markov Decision Processes

Frederic Dörband: A general approach to determinisation of weighted automata

We introduce a general framework for determinisation of weighted automata (WA) over semirings which we call M-sequentialisation. The parameter M is a monoid and determines the granularity of the determinisation. Our framework includes classical determinisation, sequentialisation of automata using only a single operation, and crisp-determinisation. Moreover, we provide an M-sequentialisation construction which is applicable to a substantial class of WA, including finitely M-ambiguous WA and WA over idempotent semirings, with additional conditions on M. We show that every WA in this class is M-sequentialisable if it fulfills our notion of the twinning property.

Thomas Feller: On Logics and Homomorphism Closure

Predicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characterizing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomorphism closure (homclosure) of the class of all (finite or arbitrary) models of logical sentences: membership of structures in a sentence’s homclosure; sentence homclosedness; homclosure characterizability in a logic; normal forms for homclosed sentences in certain logics. For a wide variety of fragments of first- and second-order predicate logic, we clarify these problems’ computational properties.

Simon Jantsch: Witnessing subsystems for probabilistic systems with low tree width

Session 5: Combinatory Categorial Grammars + Description Logics II

Lena Schiffer: Parsing CCG with substitution rules and improved complexity

We propose a new parsing algorithm for Combinatory Categorial Grammar (CCG), which is a formalism that is well-established in computational linguistics. CCG is mildly context-sensitive, so it is efficiently parsable and reaches an expressiveness that is conjectured to be suitable for modeling natural languages. We extend and improve the algorithm of Kuhlmann and Satta (2014) in three aspects. First, to our knowledge this is the first CCG parsing algorithm that can handle not only application and composition rules, but also substitution rules. Second, we not only give a recognition algorithm that returns a yes-or-no answer, but we describe the retrieval of the CCG derivation tree from the parse tree. Third, when regarding the grammar as part of the input, time complexity is exponential only in the maximum rule degree of the grammar, and not in the maximum length of lexical categories or lexical arguments. Our parsing algorithm therefore paves the way for a better understanding of the source of complexity of CCG parsing, which has previously been shown to be EXPTIME-complete (Kuhlmann, Satta, and Jonsson, 2018). This talk is based on joint work with Marco Kuhlmann and Giorgio Satta.

Jakub Rydval: Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains

Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. To regain decidability of the DL ALC in the presence of GCIs, quite strong restrictions, in sum called omega-admissibility, were imposed on the concrete domain. On the one hand, we generalize the notion of omega- admissibility from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissibility to well-known notions from model theory. In particular, we show that finitely bounded homogeneous structures yield omega-admissible concrete domains. This allows us to show omega- admissibility of concrete domains using existing results from model theory. When integrating concrete domains into lightweight DLs of the EL family, achieving decidability is not enough. One wants reasoning in the resulting DL to be tractable. This can be achieved by using so-called p-admissible concrete domains and restricting the interaction between the DL and the concrete domain. We investigate p-admissibility from an algebraic point of view. Again, this yields strong algebraic tools for demonstrating p-admissibility. In particular, we obtain an expressive numerical p-admissible concrete domain based on the rational numbers. Although omega-admissibility and p-admissibility are orthogonal conditions that are almost exclusive, our algebraic characterizations of these two properties allow us to locate an infinite class of p-admissible concrete domains whose integration into ALC yields decidable DLs.

Session 5: Constraint Satisfaction Problems

Simon Knäuer: Network satisfaction for symmetric relation algebras with a flexible atom

Robin Hirsch posed in 1996 the Really Big Complexity Problem: classify the computational complexity of the network satisfaction problem for all finite relation algebras A. We provide a complete classification for the case that A is symmetric and has a flexible atom; the problem is in this case NP-complete or in P. If a finite integral relation algebra has a flexible atom, then it has a normal representation 𝔅. We can then study the computational complexity of the network satisfaction problem of A using the universal-algebraic approach, via an analysis of the polymorphisms of 𝔅. We also use a Ramsey-type result of Nešetřil and Rödl and a complexity dichotomy result of Bulatov for conservative finite-domain constraint satisfaction problems.

Florian Starke: CSPs with finite duality closed under primitive positive constructions

Primitive positive constructions are a important tool to find reductions between CSPs. Rossmann showed in 2008 that a CSP is in AC₀ if and only if its template has finite duality, i.e., a structure A has finite duality if there is a finite set of structures F such that the structures that have a homomorphism into A are precisely those into which no structure from F has a homomorphism. Our goal is to show that a CSP with template A can be primitively positively constructed from a finite structure with finite duality is if and only if A cannot primitively positively construct ({0,1},0,1,≤) or any directed cycle of length at least 2.