DL 2025: DESCRIPTION LOGICS 2025
PROGRAM FOR FRIDAY, SEPTEMBER 5TH
Days:
previous day
next day
all days

View: session overviewtalk overview

09:00-10:20 Session 7: New Perspectives on Query Containment and Controllability

Invited Talk

09:00
What It's Like to Be a Database Theorist in the Land of Multisets

ABSTRACT. I originally planned to spend this talk tackling two classic decision problems from database theory—the Query Determinacy Problem and the Query Containment Problem—in their multiset (rather than set) incarnations. Reality intervened: one hour is not four, so I will focus almost entirely on the multiset version of the Query Containment Problem. This problem has been worked on for more than 35 years, consuming hundreds of research‐person‐years, yet resulting in surprisingly few publications. By conventional academic metrics, this makes it an unwise career choice. Fortunately, what it lacks in paper count, it makes up for in the occasional flash of unexpected mathematical beauty. I will share some of these results and the stories behind them. Regrettably, I will say little about the multiset version of the Query Determinacy Problem—the gateway through which I wandered from the set‐semantics world into the land of multisets—but perhaps that will be a tale for another day.

10:00
No Cliques Allowed: The Next Step Towards BDD/FC Conjecture (Extended Abstract)

ABSTRACT. This paper addresses one of the fundamental open questions in the realm of existential rules: the conjecture on the finite controllability of bounded derivation depth rule sets, BDD/FC. We take a step toward a positive resolution of this conjecture by demonstrating that universal models generated by BDD rule sets cannot contain arbitrarily large tournaments (arbitrarily directed cliques) without entailing a loop query E(x,x) (with x existentially quantified). This simple yet elegant result narrows the space of potential counterexamples to the BDD/FC conjecture.

10:20-10:30 Poster Announcements

Enamul Haque, David Toman and Grant Weddell

Reliable Reference for a DL Knowledge Base under Data Update (abstract)

Michal Sochański, Przemysław Andrzej Wałęga and Michal Zawidzki

Two Types of Definite Descriptions: Theory and Implementation (abstract)

Tobias John, Einar Broch Johnsen, Eduard Kamburjan and Dominic Steinhöfel

Testing Description Logic Reasoners (Extended Abstract) (abstract)

10:30-11:00Coffee Break
11:00-12:20 Session 8: Rules, Guards, and Expressive Fragments
11:00
Restricted Chase Termination: You Want More than Fairness (Extended Abstract)

ABSTRACT. The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for many chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative to reduce the hardness of universal termination.

11:20
Ontology-Based Query Answering over Datalog-Expressible Rule Sets is Undecidable (Extended Abstract)

ABSTRACT. Ontology-based query answering is a problem that takes as input a set of facts F, an ontology R (typically expressed by existential rules), a Boolean query q , and asks whether R and F entails q. This problem is undecidable in general, and a widely investigated approach to tackle it is called query rewriting: from (R,q) (a ``rule query'') is computed q_R such that for any set of facts F, it holds that R and F entail q iff F entails q_R. The literature mostly focused on q_R expressed as a union of conjunctive queries (UCQs), and an algorithm that such a q_R whenever it exists has been proposed in the literature.

However, UCQ-rewritability is applicable only in restricted settings. This raises the question whether such a generic algorithm can be designed for a more expressive language, such as datalog. We solve this question by the negative, by studying the difference between datalog-expressibility and datalog-rewritability. In particular, we show that query answering under datalog-expressible rule queries is undecidable.

11:40
On Homogeneous Models of Fluted Languages (Extended Abstract)

ABSTRACT. The fluted fragment is a fragment of first-order logic in which variable quantification coincides with the order in which those variables appear as arguments in predicates and is often viewed as a multi-variable non-guarded extensions to various systems of description logics lacking role-inverses. In this paper we show that satisfiable sentences of the aforementioned language (even under reasonable extensions) admit special kinds of `nice' models we call globally/locally homogenous. Studying homogenous models allows us to simplify the methodology used for fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the two-variable sub-fragment is NExpTime-complete and Tower-complete in the general case. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have an co-r.e.-complete general (and r.e.-complete finite) satisfiability problem when augmented with counting quantifiers. Additionally, the satisfiability problem becomes complete for the first level of the analytical hierarchy if periodic counting quantifiers are permitted.

12:00
Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Abstract)

ABSTRACT. We study the Guarded Fragment with Regular Guards RGF which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying the maximal, in some natural sense, ExpSpace-complete fragment of RGF.

12:20-12:30 Poster Announcements

Sławomir Kost and Barbara Morawska

Around unification in FL\_bottom -- three related problems (abstract)

Barbara Morawska, Dariusz Marzec, Sławomir Kost and Michał Henne

FILO: unification solver for FL_0 (Extended Abstract) (abstract)

Zekeri Adams, Martin Homola and Ján Kl'Uka

Can Full Set-Theoretical Subsumption Semantics in Metamodelled Description Logics Be Captured Within Decidable FOL Fragments? (abstract)

12:30-14:00Lunch Break
14:00-15:30 Session 9: Poster Session II
Can Full Set-Theoretical Subsumption Semantics in Metamodelled Description Logics Be Captured Within Decidable FOL Fragments?

ABSTRACT. Abstract

Metamodelling in ontologies enables the structured representation of complex domains by defining relationships between concepts across multiple levels of abstraction. Subsumption, a core relation in hierarchical reasoning, provides a strong foundation for organizing ontological knowledge. In this work, we build on an extended form of higher-order description logic, denoted HIRS*(L), which supports metamodeling through two semantically fixed roles: instanceOf and subClassOf. These roles explicitly enforce meta-level constraints, allowing for a richer and more expressive representation of both hierarchical and meta-level concepts. While the logic has four known variants with three shown to be decidable, the decidability of the full set-theoretical semantics of the subClassOf relation for all concepts remains open. This work investigates the decidability of the HIRS_{SA}(L) variant by seeking to align it with well-established decidable fragments of first-order logic.

FILO: unification solver for FL_0 (Extended Abstract)

ABSTRACT. In this paper we present FILO, the first application that decides the unification problem for the description logic FL_0. FL_0 is a restricted description logic that allows only conjunction, the top constructor and value restrictions to construct complex concepts from a set of concept names (unary predicates) and role names (binary predicates). Unification of concepts in Description Logics has been proposed as a non-standard reasoning task that can help eliminate redundancies from ontologies. Unification problem in FL_0 is ExpTime complete. FILO is based on an algorithm that is exponential only in the worst case.

Around unification in FL\_bottom -- three related problems

ABSTRACT. In this paper we present three results concerning the unification problem in the description logic FL\_bottom. FL\_bottom is a sub-Boolean logic that supports only conjunction, value restrictions and the top and bottom constructors, without any form of negation; subsumption in FL\_bottom can be decided in polynomial time. Although we do not solve the unification problem itself, we establish three related findings. First, we show that unification in FL\_bottom is of type nullary, a result inspired by a similar theorem for the modal logic K. Second, we reduce the unification problem in FL\_bottom to the unification problem in FL\_0 equipped with a forward-closed TBox. Third, we prove that the matching problem in FL\_bottom can be solved in polynomial time.

Testing Description Logic Reasoners (Extended Abstract)

ABSTRACT. Ontologies rely on a vast ecosystem of software tools, especially the description logic reasoners. Yet, tool developers and maintainers have little support to ensure tool reliability. This extended abstract reports on two testing studies on EL reasoners, summarizing results from two approaches presented at ISSRE’24, ESWC’25 and preliminary results building on this work. We demonstrate how recent advances in test case generation for highly structured and constrained inputs can support software developers in the semantic web field. We develop input generators for the OWL EL profile, and report on 23 bugs we found in HermiT, ELK and Pellet, as well as the EL profile checker of the OWL-API, all using automated testing.

The ontocomc ontology: A Semantic Framework for Hindemith’s Harmonic System

ABSTRACT. Ontological representation of music concepts is a growing area of research in both the data science and computational musicology communities. This paper introduces the ontocomc ontology, a scheme that focuses on tone simultaneities, sequences of chords and their automated semantic annotation. Our ontology is based on Paul Hindemith's theory in his Craft of Musical Composition, an original construction completely at odds with traditional tonal harmony. A key characteristic of this scheme is its handling all conceivable simultaneities in a uniform way. This harmonic system has received very little (if any) attention in past data science research; in this sense, our approach constitutes a major novelty, leveraging the representational power of ontologies in conjunction with Hindemith's exhaustive classification of tone simultaneities. Chord sequences and their constituent parts are enriched with semantic features enabling SPARQL querying to capture and analyze distinctive stylistic patterns on the music surface. This process may provide valuable insights on the style, structure or emotional content of a music piece and can be used as part of feature engineering to machine learning applications.

Reliable Reference for a DL Knowledge Base under Data Update

ABSTRACT. Earlier work has shown how Russell's notion of proper definite descriptions can be captured as referring expressions: concept descriptions that are known to be singular. Concept descriptions are a more general and transparent way of communicating answers to queries. In general, how long such answers can be relied on will depend on how long facts about entities are not altered via data update, that is, on revisions to the underlying ABox of a KB. In this paper, we show how a simple variety of dynamic constraints can be added to a KB to ensure user specified durations on how long query answers must be able to be relied on.

Two Types of Definite Descriptions: Theory and Implementation

ABSTRACT. We investigate extensions of description logics with operators for definite descriptions - expressions intended to uniquely refer to elements based on their properties. Building on recent developments in both modal and description logics, we introduce two extensions of ALC, namely ALCi^l and ALCi^g, incorporating definite description operators from recent literature. We compare their expressive power and develop tableau-based decision procedures for both. Our ongoing work includes implementing these tableaux and conducting experimental evaluations to assess their practical viability in knowledge representation scenarios.

Description Logics with Epsilon Individuals

ABSTRACT. We investigate the extension of description logics (DLs) with definite descriptions—that is, references to individuals based on a description of their properties. Specifically, we introduce the syntax and semantics for epsilon-individuals, modelled on the epsilon-terms that Hilbert introduced for first order logic. We present sound and complete reasoning algorithms for the logics that result from adding epsilon-individuals to several well-known DLs. In particular, for the extension of the basic DL ALC with epsilon-individuals, we give a tableau calculus, and show that the language without TBoxes is equivalent in expressivity to the language with TBoxes, which share EXPTIME-completeness of reasoning. In the case of the extension of the language ALCO with nominals, we give a reduction to the language ALCOu with universal roles and show that reasoning remains EXPTIME-complete. Finally, for light-weight DL ELO, we show that the usual saturation calculus can be extended for epsilon-individuals, while maintaining the PTIME complexity.

Accessing Semistructured Data with KGs and LLMs

ABSTRACT. We demonstrate a principled way to query semistructured data by integrating natural language processing capabilities into knowledge graph generation. We instantiate RML mappings with LLM queries to extract ontological terms from plain text. We evaluate our approach on pharmaceutical data in JSON format.

15:30-16:00Coffee Break
16:00-17:30 Session 10: Temporal and Probabilistic Reasoning
16:00
Analysing Temporal Reasoning in Description Logics Using Formal Grammars (Extended Abstract)

ABSTRACT. We establish a correspondence between (fragments of) TEL[Next], a temporal extension of EL with the LTL operator Next^k , and conjunctive grammars (context-free grammars equipped with the operation of intersection). This connection implies that TEL[Next] does not enjoy ultimate periodicity of models, and further leads to undecidability of query answering in TEL[Next], closing a question left open since the introduction of TEL[Next]. It also allows to establish decidability of query answering for some new fragments of TEL[Next], and to reuse for this purpose existing tools and algorithms for conjunctive grammars.

16:20
Complexity of containment for conjunctive LTL queries

ABSTRACT. We investigate the computational complexity of the containment problem for conjunctive queries given in linear temporal logic LTL with the operators ‘eventually’ and ‘next-time’. We show that this problem is coNP-complete and identify a few restricted query classes for which containment is tractable (in LogSpace).

16:40
Maximum Entropy Reasoning via Model Counting in (Description) Logics that Count (Extended Abstract)

ABSTRACT. This extended abstract reports on work that was published in the proceedings of FLAIRS-38. In previous work it was shown that the logic ALC^{ME}, which extends the description logic (DL) ALC with probabilistic conditionals, has domain-lifted inference. In the FLAIRS-38 paper, we extend this result from the base logic ALC to two logics that can count, the two-variable fragment C2 of first-order logic (FOL) with counting quantifiers, and the DL ALCSCC, which can formulate expressive counting constraints on role successors and is not a fragment of FOL. As an auxiliary result, we prove that model counting in ALCSCC can be realized in a domain-liftable way.

17:00
Inconsistency Handling in DatalogMTL (Extended Abstract)

ABSTRACT. This extended abstract summarizes our IJCAI’25 paper on inconsistency handling in DatalogMTL, an extension of Datalog with metric temporal operators. Our work extends existing notions of conflicts and repairs to DatalogMTL and studies their properties. We also study the data complexity of the tasks of generating a single conflict / repair and query entailment under repair-based semantics.