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
13:00  13:15 
Reception and announcements 
Session 1: Description Logics I Chair: Lena Schiffer Zoom: link 

13:15  14:00 
Filippo De Bortoli 
14:00  14:15  Break 
14:15  15:00 
Willi Hieke Counter Model Transformation for Explaining NonSubsumption in EL 
15:00  15:30  Break 
15:30  16:00 
Christian Alrabbaa 
16:00  17:00  PI discussion 
Thursday, October 7
Session 2: Weighted Automata I Chair: Simon Knäuer Zoom: link 

13:00  13:45 
Gustav Grabolle 
13:45  14:00  Break 
14:00  14:45 
Kevin Stier 
14:45  15:00  Break 
Session 3: Weighted Automata II + Markov Decision Processes Chair: Jakub Rydval Zoom: link 

15:00  15:45 
Frederic Dörband 
15:45  16:00  Break 
16:00  16:30 
Thomas Feller 
16:30  17:00 
Simon Jantsch Witnessing subsystems for probabilistic systems with low tree width 
17:00  18:00  PI discussion 
Friday, October 8
Session 4: Combinatory Categorial Grammars + Description Logics II Chair: Kevin Stier Zoom: link 

13:00  13:45 
Lena Schiffer 
13:45  14:00  Break 
14:00  14:45 
Jakub Rydval Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains 
14:45  15:00  Break 
Session 5: Constraint Satisfaction Problems Chair: Frederic Dörband Zoom: link 

15:00  15:45 
Simon Knäuer Network satisfaction for symmetric relation algebras with a flexible atom 
15:45  16:00  Break 
16:00  16:30 
Florian Starke CSPs with finite duality closed under primitive positive constructions 
16:30  17:00 
Final remarks and farewell 
17:00  18:00  PI discussion 
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 rolesuccessor 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 ExpTimecomplete decision problem (Baader, Bednarczyk & Rudolph, 2020). The upper bound proof uses an algorithm based on type elimination, which runs in bestcase 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 realworld 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 bestcase 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 NonSubsumption in EL
When subsumption relationships unexpectedly fail to be detected by a description logic reasoner, the cause for this “nonentailment” 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 nonentailments. Explaining nonentailments 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 Msequentialisation. 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 crispdeterminisation. Moreover, we provide an Msequentialisation construction which is applicable to a substantial class of WA, including finitely Mambiguous WA and WA over idempotent semirings, with additional conditions on M. We show that every WA in this class is Msequentialisable 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 nontrivial 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 secondorder predicate logic, we clarify these problems’ computational properties.
Simon Jantsch: Witnessing subsystems for probabilistic systems with low tree width
Friday, October 8
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 wellestablished in computational linguistics. CCG is mildly contextsensitive, 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 yesorno 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 EXPTIMEcomplete (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 omegaadmissibility, 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 omegaadmissibility to wellknown notions from model theory. In particular, we show that finitely bounded homogeneous structures yield omegaadmissible 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 socalled padmissible concrete domains and restricting the interaction between the DL and the concrete domain. We investigate padmissibility from an algebraic point of view. Again, this yields strong algebraic tools for demonstrating padmissibility. In particular, we obtain an expressive numerical padmissible concrete domain based on the rational numbers. Although omegaadmissibility and padmissibility are orthogonal conditions that are almost exclusive, our algebraic characterizations of these two properties allow us to locate an infinite class of padmissible 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 NPcomplete 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 universalalgebraic approach, via an analysis of the polymorphisms of 𝔅. We also use a Ramseytype result of Nešetřil and Rödl and a complexity dichotomy result of Bulatov for conservative finitedomain 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_{0} 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.