Frontiers of Combining Systems. 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 – October 1, 2025, Proceedings

René Thiemann, Christoph Weidenbach

► To cite this version:

René Thiemann, Christoph Weidenbach. Frontiers of Combining Systems. 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 – October 1, 2025, Proceedings. 15th International Symposium Frontiers of Combining Systems, Sep 2025, Reykjavik, Iceland. 15979, Springer Nature Switzerland, 2026, Lecture Notes in Computer Science, 978-3-032-04166-1. 10.1007/978-3-032-04167-8. hal-05470956

HAL Id: hal-05470956

https://hal.science/hal-05470956v1

Submitted on 22 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
René Thiemann

Christoph Weidenbach (Eds.)

LNAI 15979

# Frontiers of Combining Systems

15th International Symposium, FroCoS 2025

Reykjavik, Iceland, September 29 – October 1, 2025

Proceedings

<figure><img src="image_2.png" /></figure>

Springer

OPEN ACCESS
Founding Editor

Jörg Siekmann

Series Editors

Randy Goebel, University of Alberta, Edmonton, Canada

Wolfgang Wahlster, DFKI, Berlin, Germany

Zhi-Hua Zhou, Nanjing University, Nanjing, China
The series Lecture Notes in Artificial Intelligence (LNAI) was established in 1988 as a topical subseries of LNCS devoted to artificial intelligence.

The series publishes state-of-the-art research results at a high level. As with the LNCS mother series, the mission of the series is to serve the international R & D community by providing an invaluable service, mainly focused on the publication of conference and workshop proceedings and postproceedings.
René Thiemann · Christoph Weidenbach
Editors

Frontiers of
Combining Systems

15th International Symposium, FroCoS 2025
Reykjavik, Iceland, September 29 – October 1, 2025
Proceedings

<figure><img src="image_3.png" /></figure>

Springer
Editors

René Thiemann

University of Innsbruck

Innsbruck, Austria

Christoph Weidenbach

<figure><img src="image_4.png" /></figure>

Max-Planck-Institut für Informatik

Saarbrücken, Germany

<figure><img src="image_5.png" /></figure>

ISSN 0302-9743

ISSN 1611-3349 (electronic)

Lecture Notes in Artificial Intelligence

ISBN 978-3-032-04166-1

ISBN 978-3-032-04167-8 (eBook)

https://doi.org/10.1007/978-3-032-04167-8

LNCS Sublibrary: SL7 – Artificial Intelligence

© The Editor(s) (if applicable) and The Author(s) 2026. This book is an open access publication.

**Open Access** This book is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use.

The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This Springer imprint is published by the registered company Springer Nature Switzerland AG
The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

If disposing of this product, please recycle the paper.
Preface

These proceedings contain the papers selected for presentation at the 15th *International Symposium on Frontiers of Combining Systems* (FroCoS 2025). The symposium was held during September 29 – October 1, 2025 at ICE-TCS, the theoretical computer science lab of Reykjavik University, Iceland. It was co-located with the 34th *International Conference on Automated Reasoning with Analytic Tableaux and Related Methods* (TABLEAUX 2025) and the 16th *International Conference on Interactive Theorem Proving* (ITP 2025).

FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis.

FroCoS 2025 received 32 submissions. Each paper was evaluated by the members of the Program Committee who did a great job at thoroughly evaluating these submissions regarding their technical and presentational quality and providing helpful feedback to the authors. Reviewing was single-blind and each paper was subject to at least three reviews, followed by sometimes extensive discussions within the Program Committee. In the end, 21 papers were selected for presentation at the symposium and for publication. We have grouped them in this volume according to the following topic classification: (1) description logics, (2) beyond classical logic, (3) satisfiability modulo theories (SMT), (4) term rewriting systems, (5) theorem proving, (6) specific reasoning procedures, and (7) proof checking.

Together with the Program Committee, we considered suitable candidates to give an invited talk, and were delighted to find two outstanding invited speakers:

- Kaustuv Chaudhuri, LIX, Inria/École Polytechnique (joint with TABLEAUX)

- Carsten Fuhs, Birkbeck, University of London

We would like to thank all the people who contributed to making FroCoS 2025 a success. In particular, we thank the members of the Program Committee and the external reviewers for their excellent, timely work and for providing the authors with insightful feedback. Of course we thank the authors for submitting high-quality papers, taking the reviewers' feedback into account, and presenting their work in a way that is accessible to the broad FroCoS audience. Next, we thank the invited speakers for their inspiring talks. Moreover, we thank the local organizers and the theoretical computer science lab of Reykjavik University for organizing and supporting FroCoS. Finally, we gratefully acknowledge financial support from Springer.

July 2025

René Thiemann
Christoph Weidenbach
# Organization

## Program Committee Chairs

René Thiemann

University of Innsbruck, Austria

Christoph Weidenbach

Max Planck Institute for Informatics, Germany

## Steering Committee

Franz Baader

TU Dresden, Germany

Andreas Herzig

University of Toulouse, France

Boris Konev

University of Liverpool, UK

Andrei Popescu

University of Sheffield, UK

Giles Reger

Amazon Web Services, USA & University of
Manchester, UK

Ulrike Sattler

University of Manchester, UK

Martin Suda

České vysoké učení technické v Praze, Czech
Republic

## Program Committee

Franz Baader

TU Dresden, Germany

Haniel Barbosa

Universidade Federal de Minas Gerais, Brazil

Jasmin Blanchette

LMU München, Germany

Cyril Cohen

Inria, ENS de Lyon, France

Clare Dixon

University of Manchester, UK

Mathias Fleury

Universität Freiburg, Germany

Silvio Ghilardi

Università degli Studi di Milano, Italy

Jürgen Giesl

RWTH Aachen, Germany

Alberto Griggio

Fondazione Bruno Kessler, Italy

Andreas Herzig

IRIT, CNRS, University of Toulouse, France

Boris Konev

University of Liverpool, UK

Georg Moser

University of Innsbruck, Austria

Lawrence Paulson

University of Cambridge, UK

Elaine Pimentel

University College London, UK

Andrei Popescu

University of Sheffield, UK

Andrew Reynolds

University of Iowa, USA
Christophe Ringeissen

Philipp Rümmer

Uli Sattler

Renate A. Schmidt

Roberto Sebastiani

Viorica Sofronie-Stokkermans

Martin Suda

Akihisa Yamada

Inria Nancy, France

University of Regensburg, Germany

University of Manchester, UK

University of Manchester, UK

Università di Trento, Italy

Universität Koblenz, Germany

České vysoké učení technické v Praze, Czech Republic

AIST, Japan

## Local Organizers

Tarmo Uustalu

Antonis Achilleos

Bjarki Gunnarsson

Vasiliki Kyriakou

Calvin Santiago Lee

Yasuaki Morita

Jacob Neumann

Reykjavik University, Iceland

Reykjavik University, Iceland

University of Iceland, Iceland

Reykjavik University, Iceland

Reykjavik University, Iceland

Reykjavik University, Iceland

Reykjavik University, Iceland

## Additional Reviewers

Carlos Aguilera Ventura

Mauricio Ayala-Rincón

Bartosz Bednarczyk

James Brotherston

Martin Desharnais

Zafer Esen

Tiago Ferreira

Carsten Fuhs

Alessandro Gianola

Roland Herrmann

Ullrich Hustadt

Jan-Christoph Kassing

Christian Lidström

Luca Maio

IRIT, CNRS, University of Toulouse, France

Universidade de Brasília, Brazil

Uniwersytet Wrocławski, Poland

University College London, UK

LMU München, Germany

Uppsala University, Sweden

Universidade Federal de Minas Gerais, Brazil

Birkbeck, University of London, UK

Universidade de Lisboa, Portugal

University of Regensburg, Germany

University of Liverpool, UK

RWTH Aachen, Germany

Fondazione Bruno Kessler, Italy

LMU München, Germany
Albert Oliveras
Magdalena Ortiz
Pedro Quaresma
Gianluca Redondi
Balazs Toth
Hongkai Yin

Universitat Politècnica de Catalunya, Spain
TU Wien, Austria
Universidade de Coimbra, Portugal
Fondazione Bruno Kessler, Italy
LMU München, Germany
Central European University, Austria
Abstracts of Invited Talks
# Towards a Universal Interactive Theorem Proving Interface

Kaustuv Chaudhuri

Inria & LIX, Institut Polytechnique Paris

**Abstract.** Interactive theorem provers are usually designed to use formal languages for expressing proofs and commands. Such languages are rarely portable across different systems, which leads to fragmentation in the community, duplication of effort, and an incumbency bias for existing systems. One way to address this incompatibility is to design an interactive proving interface where proof and command languages have a negligible role. Instead, users build proofs by manipulating the theorem itself using interaction devices such as mice and touch screens, and interaction mechanisms such as clicking, selection, dragging-and-dropping, etc.; in other words, using *direct manipulation*. There have been a number of proposals for such interfaces, most famously the *proof by pointing* approach of the 1990s [1], with several other approaches since then [8, 2, 3, 9].

This talk presents a foundational, proof theoretic, and system independent view of *direct manipulation interfaces* that generalizes these earlier attempts to *proof by linking* [5], which has been implemented in the interfaces *Profound* [6] and *Actema* [7] for first-order intuitionistic logic. These interfaces are intended to be compatible with arbitrary backend proof systems, either as plugins or as certifying procedures. For example, *Profound* can be used to produce proofs for Lean 3, Lean 4, Rocq (Coq), Isabelle/HOL, and HOL4 [4]. Linking requires the use of proof calculi of *deep inference*, which are proof systems where logical inferences are allowed in arbitrary formula contexts. This talk presents a particular kind of deep inference called *open deduction*, which was originally developed for classical logic but which is now extended and adapted to intuitionistic logic. In addition to linking, open deduction is suitable for a variety of other front-end features such as hierarchical levels of detail and refactoring by sharing subproofs. We will also discuss current work on extensions of open deduction (and linking) to support dependent type theory and induction.

## References

1. Bertot, Y., Kahn, G., Théry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) International Conference on the Theoretical Aspects of Computer Software TACS. TACS 1994. LNCS, vol. 789, pp. 141–160. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57887-0_94

2. Breitner, J.: Visual theorem proving with the incredible proof machine. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving, pp. 123–139. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_8
3. Callies, E., Laurent, O.: Click and coLLecT an interactive linear logic prover. In: 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021). Rome (virtual), Italy (2021), https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271501

4. Chaudhuri, K., Donato, P., Massacci, L., Werner, B.: Certifying proof-by-linking. Technical report, INRIA (2022). https://inria.hal.science/hal-04317972

5. Chaudhuri, K.: Subformula linking as an interaction method. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Proceedings of the 4th Conference on Interactive Theorem Proving (ITP). LNCS, vol. 7998, pp. 386–401. Springer, Cham (2013)

6. Chaudhuri, K.: Subformula linking for intuitionistic logic with application to type theory. In: Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction. LNCS, vol. 12699, pp. 200–216. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_12

7. Donato, P., Strub, P., Werner, B.: A drag-and-drop proof tactic. In: Popescu, A., Zdancewic, S. (eds.) 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 197–209. ACM (2022). https://doi.org/10.1145/3497775.3503692

8. Lerner, S., Foster, S.R., Griswold, W.G.: Polymorphic blocks: formalism-inspired UI for structured connectors. In: 33rd Annual ACM Conference on Human Factors in Computing Systems, pp. 3063–3072. Association for Computing Machinery, New York, NY, USA (2015). https://doi.org/10.1145/2702123.2702302

9. Reis, G., Naeem, Z., Hashim, M.: Sequoia: a playground for logicians - (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol. 12167, pp. 480–488. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_32
# Automated Static Program Analysis via Constrained Term Rewriting

Carsten Fuhs

University of London, UK

c.fuhs@bbk.ac.uk

**Abstract.** Static program analysis is a way of determining whether a program has certain desirable properties without actually running the program. Over the last decades, static analysis has made massive strides forward thanks to the ready availability of tools like SAT and SMT solvers. In this talk, I will sketch a systematic way of constructing a tool for static program analysis based on constrained rewriting, with a focus on program termination as the property of interest.

In the first part of the talk, I will discuss Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate verification language that extends classic term rewriting in several directions relevant to program analysis. LCSTRSs as a form of constrained rewrite systems allow for expressing many features of real-world programming languages:

- algebraic data types;

- built-in data types (e.g., integers, arrays) and their standard operations and constraints;

- higher-order types, as used in functional programs.

I will describe a Dependency Pair Framework for compositional analysis of termination of call-by-value evaluation for LCSTRSs. Its automation heavily benefits from existing off-the-shelf SMT solvers to tackle the search problems inherent to automated termination proving.

In the second part of the talk, I will describe a translation from a subset of Scala to constrained rewrite systems such that termination of the rewrite system implies termination of the original Scala program. In combination with a termination tool for constrained rewriting as a back-end, this approach allows for proving termination of real-world programs via tools designed for the analysis of constrained term rewriting.

This talk is based on joint work with Liye Guo, Cynthia Kop, Viktor Kunčak, and Dragana Milovančević.
# Contents

## Description Logics

The Concrete EVONNE: Visualization Meets Concrete Domain Reasoning 3
*Christian Alrabbaa, Franz Baader, Raimund Dachselt, Alisa Kovtunova, and Julián Méndez*

The Expressive Power of Description Logics with Numerical Constraints over Restricted Classes of Models 22
*Franz Baader and Filippo De Bortoli*

Reasoning in OWL 2 EL with Hierarchical Concrete Domains 40
*Francesco Kriegel*

## Beyond Classical Logic

An Analytic Representation of the Semantics of First-Order S5 63
*Matthias Baaz, Mariami Gamsakhurdia, and Anela Lolić*

Deciding Satisfiability for Overlaid Symbolic Heaps 80
*Nicolas Peltier, Quentin Petitjean, and Mihaela Sighireanu*

Subtyping in Dependently-Typed Higher-Order Logic 98
*Colin Rothgang and Florian Rabe*

## Satisfiability Modulo Theories

Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories 117
*Gabriele Masina and Roberto Sebastiani*

Shininess, Strong Politeness, and Unicorns 135
*Benjamin Przybocki, Guilherme V. Toledo, and Yoni Zohar*

Polite Combination in Parametric Array Theories 153
*Rodrigo Raya and Christophe Ringeissen*

Number Theory Combination: Natural Density and SMT 169
*Guilherme V. Toledo and Yoni Zohar*
## Term Rewrite Systems

Weighted Rewriting 191
Martin Avanzini and Akihisa Yamada

Graph-Embedded Rewrite Systems: Combination and Undecidability
Results 209
Serdar Erbatur, Andrew M. Marshall, Paliath Narendran,
and Christophe Ringeissen

Data-Driven Runtime Complexity Analysis 228
Samuel Frontull, Manuel Meitinger, and Georg Moser

Difference of Constrained Patterns in Logically Constrained Term Rewrite
Systems 247
Naoki Nishida, Misaki Kojima, and Yuto Nakamura

## Theorem Proving

Iterative Monomorphisation 269
Tanguy Bozec and Jasmin Blanchette

The Dependently Typed Higher-Order Form for the TPTP World 287
Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, and Geoff Sutcliffe

Context-Aware Clause Selection Using Symbol Name Meanings
in Theorem Proving 306
Claudia Schon

## Specific Reasoning Procedures

When GNNs Met a Word Equations Solver: Learning to Rank Equations 327
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler,
Chencheng Liang, and Philipp Rümmer

A Finite Abstraction of Real-Valued Functions for Complete Reasoning
About Influence 346
Sören Möller, Florian Bruse, and Martin Lange

## Proof Checking

Checking Linear Integer Arithmetic Proofs in Lambdapi 367
Alessio Coltellacci and Stephan Merz
Certifying rlive: A New Proof Strategy for Liveness Model Checking 386
Giulia Sindoni, Alberto Griggio, and Stefano Tonetta

Author Index 405
Description Logics
# The Concrete EVONNE: Visualization Meets Concrete Domain Reasoning

Christian Alrabbaa<fnref n="1" />(✉)D, Franz Baader<fnref n="1" />(✉)D, Raimund Dachselt<fnref n="2" />(✉)D, Alisa Kovtunova<fnref n="1" />(✉)D, and Julián Méndez<fnref n="2" />(✉)D

**Abstract.** EVONNE is a web application primarily designed to explain Description Logic (DL) entailments using an interactive visualization approach for proofs. This paper introduces an extension of EVONNE to DLs with concrete domains, which are needed for formalizing concepts whose definitions involve quantitative information. Specifically, we focus on two extensions of the DL $\mathcal{EL}_{\perp}$: one with constraints formulated as linear equations and the other with difference constraints. First, we have extended EVONNE to enable the generation and presentation of proofs involving these concrete domains. Then, leveraging the unique properties of each domain, we have designed and incorporated alternative visual explanations for the numerical parts of the proofs. Finally, we have assessed the effectiveness of these visual explanations through qualitative user studies and a performance benchmark. While opinions on one of these explanations varied, the other was widely recognized for its clarity and ease of understanding.

**Keywords:** Explainable AI · Description Logic · Concrete Domains · Visualization · Linear Equations · Difference Constraints

## 1 Introduction

Due to the opacity of many machine learning approaches such as deep neural networks [27], explainability (xAI) has become a major research field in Artificial Intelligence [18, 19]. Symbolic AI approaches based on logic have the advantage over subsymbolic approaches that they are explainable by design: a consequence computed by an automated reasoner can in principle be explained using a proof, which demonstrates how the consequence can be derived from given axioms by applying simple inference rules, and the non-derivability of a statement can (for some logics) be explained by showing a finite counter-interpretation, which is a model of all axioms, but not of the non-derivable statement. However, to leverage this advantage of logic-based approaches in practice, one must be able to produce proofs (counter-interpretations) that are appropriate for explanation purposes and present them in a comprehensible and cogent way.

<footnote n="1">¹ Institute of Theoretical Computer Science, TU Dresden, Dresden, Germany {christian.alrabbaa,franz.baader,alisa.kovtunova}@tu-dresden.de</footnote>

<footnote n="2">² Interactive Media Lab Dresden, TU Dresden, Dresden, Germany {raimund.dachselt,julian.mendez2}@tu-dresden.de</footnote>
In ongoing work, we address these issues in the context of Description Logics (DLs) [12], which are a prominent family of logic-based knowledge representation languages frequently used to formalize ontologies for various application domains. The computation of appropriate proofs and counter-interpretations has been tackled in [3,4] and [8,9], respectively. Both means of explanation can be presented in our interactive visualization tool EVONNE<fnref n="1" />[2,23], but the proof-presentation facilities are considerably more mature. Since the publication of the EVONNE system description [2] and a journal paper emphasizing its visualization components [23], this tool has been extended by new features and the look and feel of the system has been improved considerably.

Here we concentrate on the extension of the proof visualization facilities of EVONNE to DLs with so-called concrete domains [11,22]. In particular, we consider extensions of tractable DLs of the *EL* family [10] with two p-admissible concrete domains based on rational numbers, one ($D_{Q,lin}$) that can use linear equations to formulate constraints [13] and another ($D_{Q,diff}$) based on difference constraints [10]. Such numerical constraints turn out to be very useful for describing concepts whose definition involves quantitative information, such as the battery capacity of a drone, its flight time, and weather conditions including temperature, which may influence the battery discharge rate. The exact definition of p-admissibility is not relevant for this paper (see [10,13] for details), but note that it is needed to preserve tractability. Both mentioned concrete domains are p-admissible, but their combination is not, though they can both be integrated into the same DL as long as they do not interact. In [5], we have addressed the problem of generating proofs for consequences derived from knowledge bases formulated in such DLs. Basically, the proof system for the extended DL as introduced in [10] uses entailment between and unsatisfiability of sets of concrete domain constraints as applicability conditions. The idea is then to explain the satisfaction of such side conditions by a proof of the entailment (unsatisfiability) if this is requested by the user. The first important new feature of EVONNE described in this paper is the extension of its proof presentation facilities by such concrete domain proofs and their interaction with the abstract DL proofs.

However, the most original contribution of this work lies in its introduction of novel visual explanations for unsatisfiability and entailment in the considered numerical concrete domains. These visualizations are designed to reflect the unique properties of the domains and offer more intuitive insight into the underlying numerical reasoning. In the case of $D_{Q,lin}$, unsatisfiability of a set of constraints using only two variables can be visualized in the 2D Euclidean Space by showing that the lines corresponding to the constraints do not intersect in a single point. Here, we address the challenge of extending this idea to higher dimensions. For $D_{Q,diff}$, unsatisfiability of a constraint set corresponds to the existence of a negative cycle in the difference graph induced by these constraints. Thus, we developed a visual explanation based on such cycles. A priori, it is not clear how these visual explanations compare to numerical proofs.

<footnote n="1">¹ EVONNE’s source code, documentation, and evaluation material (user studies, benchmark) are available at: https://imld.de/evonne.</footnote>
For this reason, we conducted qualitative user studies to investigate the user reception of these visualization techniques.

In summary, this paper presents the latest extension of EVONNE, enabling interactive visualization of proofs for DLs with concrete domains—crucial for modeling concepts involving quantitative constraints. We contribute: (1) the first proof visualization tool supporting DLs with linear equations and difference constraints, (2) novel domain-specific visual explanations tailored to enhance comprehension of numerical reasoning, and (3) empirical validation through user studies and benchmarks, demonstrating the effectiveness of our approach. Our assessments showed that the proposed visualizations supported users in understanding conclusions more effectively than when no explanation was provided.

# 2 Description Logics and Concrete Domains

In this section we recall the Description Logic $\mathcal{EL}_{\perp}$ [12], and its extension $\mathcal{EL}_{\perp}[\mathcal{D}]$ with a concrete domain $\mathcal{D}$ [10]. We focus on two particular concrete domains $\mathcal{D}_{\mathbb{Q},\text{diff}}$ and $\mathcal{D}_{\mathbb{Q},\text{lin}}$ [10, 13], both defined over the rational numbers $\mathbb{Q}$.

## 2.1 Concrete Domains

Concrete domains integrate reasoning about quantitative attributes of objects into DLs [11, 13, 22]. Let $\mathbb{N}$ be a set of concrete predicates, where every $\Pi \in \mathbb{N}$ has arity $n_{\Pi} \in \mathbb{N}$. A concrete domain (CD) $\mathcal{D} = (\Delta^{\mathcal{D}}, \cdot^{\mathcal{D}})$ over $\mathbb{N}$ consists of a set $\Delta^{\mathcal{D}}$ and relations $\Pi^{\mathcal{D}} \subseteq (\Delta^{\mathcal{D}})^{n_{\Pi}}$ for all $\Pi \in \mathbb{N}$. We assume that $\mathbb{N}$ always contains predicates $\perp$ and $\top$, interpreted as $\perp^{\mathcal{D}} := \emptyset$, and $\top^{\mathcal{D}} := \Delta^{\mathcal{D}}$. Let $\mathbb{N}_{\top}$ be a set of variables. A constraint $\Pi(x_1, \dots, x_{n_{\Pi}})$, with $\Pi \in \mathbb{N}$ and $x_1, \dots, x_{n_{\Pi}} \in \mathbb{N}_{\top}$, is a predicate with variables as arguments. A constraint $\alpha = \Pi(x_1, \dots, x_{n_{\Pi}})$ is satisfied by an assignment $s: \mathbb{N}_{\top} \to \Delta^{\mathcal{D}}$ if $(s(x_1), \dots, s(x_{n_{\Pi}})) \in \Pi^{\mathcal{D}}$. An implication is of the form $\mathcal{C} \to \alpha$, where $\mathcal{C}$ is a conjunction (set) of constraints. The implication is valid if all assignments satisfying all constraints in $\mathcal{C}$ also satisfy $\alpha$. A conjunction $\mathcal{C}$ of constraints is unsatisfiable iff $\mathcal{C} \to \perp$ is valid.

The CD $\mathcal{D}_{\mathbb{Q},\text{diff}}$ contains predicates $\top$, $\perp$, $x = q$, $x > q$, and $x + q = y$, for constants $q \in \mathbb{Q}$, with their natural semantics [10]. For instance, the constraint $x + q = y$ is interpreted as $(x + q = y)^{\mathcal{D}_{\mathbb{Q},\text{diff}}} = \{(p, r) \in \mathbb{Q} \times \mathbb{Q} \mid p + q = r\}$.

**Example 1.** Assume a delivery drone with $bp$ representing its current *battery percentage*. The percentage is measured at multiple checkpoints, denoted as $bp_0$, $bp_1$, $bp_2$, with constraints: $bp_0 - 0.25 = bp_1$, $bp_1 - 0.2 = bp_2$, $bp_1 > 0.3$ and $bp_2 > 0.25$. If the initial percentage ($bp_0$) equals 0.65, then not all the constraints hold, and the drone is not permitted to fly.

For $\mathcal{D}_{\mathbb{Q},\text{lin}}$, besides $\top$ and $\perp$, the predicates are given by linear equations $\sum_{i=1}^{n} a_i x_i = b$, for $a_i, b \in \mathbb{Q}$, with their natural semantics [13]. For instance, $x + y - z = 0$ is interpreted as $(x + y - z = 0)^{\mathcal{D}_{\mathbb{Q},\text{lin}}} = \{(p, q, s) \in \mathbb{Q}^3 \mid p + q = s\}$.
*Example 2.* Assume *nr* and *hr* represent the average *normal* and *high* battery discharge *rates*, respectively. Under normal conditions, the delivery drone can fly for 8 hours on a single charge with a 30Ah battery, i.e., 8*nr* = 30. In cold conditions, one hour of flight increases the battery consumption such that 4*nr* + *hr* = 30. Therefore, if a delivery requires at most 2 hours in cold temperatures, the drone can complete it on a single charge.

## 2.2 Description Logics

DLs are decidable fragments of first-order logic (FOL) with a special, variable-free syntax and use only unary and binary predicates, called *concept names* and *role names*, respectively. These are used to build *complex concepts*, which correspond to first-order formulas with one free variable, and *axioms*, which correspond to first-order sentences. In this paper we consider the lightweight DL $\mathcal{EL}_{\perp}$. We use the usual notion of *entailment*, denoted $O \models A \sqsubseteq B$, where A and B are concept names, and O is a finite set of axioms, called an *ontology*. For more details about the syntax and semantics of DLs, see [12].

The extension of $\mathcal{EL}_{\perp}$ with a concrete domain $\mathcal{D}$, i.e., $\mathcal{EL}_{\perp}[\mathcal{D}]$, is obtained by allowing constraints $\alpha$ in $\mathcal{D}$ to be used as $\mathcal{EL}_{\perp}$ concepts. As in [5], we use the notation $[\alpha]$ to distinguish between constraints and classical concepts. For instance, the statement that a *delivery drone* has a battery with a battery percentage greater than 0.25 can be expressed in an $\mathcal{EL}_{\perp}[\mathcal{D}_{\mathcal{Q},\text{diff}}]$ axiom as $\mathrm{DD} \sqsubseteq \exists \mathrm{has.}(\mathrm{Battery} \sqcap [bp > 0.25])$.

# 3 Combined Proofs

EVONNE is a web application designed to explain DL entailments. It supports multiple proof types [2] and enhances them with interactive visualizations, helping users understand entailments and debug ontologies [23]. Proofs in EVONNE are generated using the EVVE library [7], and follow the notion introduced in [3]: A proof *P* of *O* *models* A *sqsubseteq* B if and only if there is a finite, acyclic, directed *hypergraph*, where each vertex *v* is labeled with an axiom *ℓ*(*v*). Hyperedges are of the form (*S*, *d*), where *S* is a set of vertices and *d* is a vertex such that {*ℓ*(*v*) | *v* ∈ *S*} *models* *ℓ*(*d*). The leaf vertices of a proof are labeled with axioms from *O*, and the root with A *sqsubseteq* B. EVONNE visualizes the proof hypergraphs using *tree* structures. In this paper, we extend EVONNE’s proofs to cover *combined proofs* for $\mathcal{EL}_{\perp}[\mathcal{D}_{\mathcal{Q},\text{diff}}]$ and $\mathcal{EL}_{\perp}[\mathcal{D}_{\mathcal{Q},\text{lin}}]$ entailments. The following example demonstrates the approach, as introduced in [5].

Let $O = \{A \sqsubseteq [\alpha_1], A \sqsubseteq [\alpha_2], A \sqsubseteq [\alpha_3], [\beta] \sqsubseteq B\}$ be an ontology such that $O \models A \sqsubseteq B$. First, we identify the relevant constraints in *O* and establish implications between them in order to build the subsumption hierarchy of abstract concepts. By using an appropriate CD reasoner, we test relevant implications such as $\{\alpha_1, \alpha_2\} \rightarrow \beta$. The ontology is then extended with axioms that encode all the valid relevant implications, i.e., $O' = O \cup \{[\alpha_1] \sqcap [\alpha_2] \sqsubseteq [\beta], \dots\}$. By classifying $O'$ we obtain $O' \models A \sqsubseteq B$. Lastly, by integrating the proof of $\{\alpha_1, \alpha_2\} \rightarrow \beta$
in the proof of $O' \models A \sqsubseteq B$ as a proof for $[\alpha_1] \sqcap [\alpha_2] \sqsubseteq [\beta]$, we obtain the combined proof for $O \models A \sqsubseteq B$.

*Example 3.* Consider the delivery drone (DD) from Example 2, along with the concept name *large battery drone* (LBD). Additionally, assume the following information is given. First, if operating at a high discharge rate for two hours draws 30Ah, this implies that a drone has a large battery, i.e., $[2hr = 30] \sqsubseteq$ LBD. Second, the delivery drone satisfies the constraints shown in Example 2, i.e., $DD \sqsubseteq [8nr = 30] \sqcap [4nr + hr = 30]$. From these two axioms, it follows that the delivery drone is a large battery drone, i.e., $DD \sqsubseteq$ LBD. An explanation of this conclusion is provided by the combined proof shown in Fig. 1a, where the proof in Fig. 1b shows the inferences at the level of equations.

To complete the picture of how concrete domain-dependent entailments are proven, we now describe the procedures that handle the CD reasoning steps.

*Reasoning in $D_{Q,lin}$.* Deciding the validity of $\mathcal{C} \to \beta$ is achieved by identifying linear combinations that allow $\beta$ to be derived from the equations in $\mathcal{C}$. For instance, the implication $\{8nr = 30, 4nr + hr = 30\} \to hr = 15$ can be shown by multiplying $8nr = 30$ by $-\frac{1}{2}$ and adding it to $4nr + hr = 30$. Similarly, the unsatisfiability of a system of equations can be shown by providing a linear combination that results in the derivation of $0 = c$, where $c \neq 0$. In [5], determining the coefficients for the linear combinations is achieved using Gaussian Elimination, and these coefficients are used to build the inferences that constitute the proof. An example of a $D_{Q,lin}$ proof in EVONNE is shown in Fig. 1b

*Reasoning in $D_{Q,diff}$.* Unlike the reasoning process in $D_{Q,lin}$, deciding the validity of $\mathcal{C} \to \beta$ is based on the saturation of $D_{Q,diff}$ constraints, using the rules shown in [5, Fig. 1]. Thus, checking whether $\mathcal{C} \to \beta$ is valid is done by checking if the implication is present in the result of the saturation. In addition, if $\beta$ is of the form $x > q$, then the implication is valid if either (i) $x = q'$ where $q' > q$ or (ii) $x > q'$ where $q' \ge q$ are derived with the saturation rules. A proof of $D_{Q,diff}$ entailment is thus built using the instantiations of saturation rules directly. An example of such a proof in EVONNE is shown in Fig. 1c

Combined proofs do not depend on the nature of the domains, making them versatile explanations that can be applied to various logics and concrete domains. However, their level of detail can result in large structures with potentially complicated inferences. For instance, the more variables and constraints involved in an entailment, the larger the resulting proof. To address this, we introduce alternative visual explanations, which we discuss in Sect. 4.

# 4 Domain-Specific Visualizations

In this section, we introduce two alternative visual explanations that leverage the specific characteristics of each concrete domain to present numerical entailments differently. These explanations do not rely on the DL part of the ontology, making them applicable to other logics or formalisms that incorporate these domains.
<figure><img src="image_6.png" /><figcaption>Fig. 1. Examples of proofs in EVONNE.</figcaption></figure>

## 4.1 Explanations of $\mathcal{D}_{\mathbb{Q},\text{lin}}$ Entailments

Let $\beta$ be a linear equation, and $\mathcal{C}$ be a set of linear equations such that $\mathcal{C} \to \beta$. The implication means that every assignment satisfying all the constraints in $\mathcal{C}$, i.e., every solution, also satisfies $\beta$. A proof explains the implication by showing how the conclusion $\beta$ is derived from equations in $\mathcal{C}$, i.e., showing that all solutions to $\mathcal{C}$ are also solutions to $\beta$. Hence, a compact representation showing every solution to $\mathcal{C}$ is a solution to $\beta$ offers an alternative way to explain the implication.

If we consider systems of linear equations with at most two variables, which are shared across all equations (e.g., $\{\alpha_1, \dots, \alpha_n, \beta\}$), then we can use lines in the 2D Euclidean Space to achieve a compact representation of all solutions to the equations, as each solution corresponds to a point in the 2D space. For example, assume $\{\alpha_1, \dots, \alpha_n\} \to \beta$. If $\beta = \perp$, this means that the system $\{\alpha_1, \dots, \alpha_n\}$ has no solutions. In other words, the lines corresponding to $\alpha_1, \dots, \alpha_n$ neither intersect at a single point nor overlap. On the other hand, if $\beta \neq \perp$ and $\{\alpha_1, \dots, \alpha_n\}$ is satisfiable, then the system $\{\alpha_1, \dots, \alpha_n, \beta\}$ either has a unique solution, i.e., exactly one point where all the lines intersect, or infinitely many solutions, i.e., all lines overlap. Therefore, by demonstrating the existence or absence of such intersections, we can explain entailments effectively.

Using dimensionality reduction, we can apply the same idea to equations with more than two variables. While there are multiple ways to achieve dimensionality reduction [15], we utilize the solution space of a system of equations to project the $n$-dimensional equations to 2D. Let $\mathcal{C}$ be a set of equations where $\mathcal{C} \to \beta$, let $s$ be a solution to $\mathcal{C}$, and let $x$ and $y$ be any two variables appearing in $\beta$. By replacing all the variables, except $x$ and $y$, in all equations with their corresponding values in $s$, we obtain equations involving at most two variables. The resulting equations can be viewed as a snapshot of $\mathcal{C}$ with respect to $s$, focusing on $x$ and $y$. Therefore, in a plane defined by $x$ and $y$, and since $s$ is a solution, all the lines must intersect. Hence, we can explain $\mathcal{C} \to \beta$ by showing that for every solution $s$ and every plane
<figure><img src="image_7.png" /><figcaption>Fig. 2. $\mathcal{D}_{\mathbb{Q},\text{lin}}$ implication of $3x_1 - 3x_2 - x_3 + 3x_4 = 7$ in EVONNE.</figcaption></figure>

defined by $x$ and $y$, the intersection of all the lines of $\mathcal{C}$ is the same intersection of the line corresponding to $\beta$ and the lines of $\mathcal{C}$.

To explain unsatisfiability, we can use a similar approach. If $\mathcal{C} \to \perp$, then there must be a contradiction in $\mathcal{C}$. More specifically, at least two contradictory equations must be derivable from $\mathcal{C}$, i.e., equations of the form $X = q$ and $X = p$, where $X$ is a sum of terms and $p, q \in \mathbb{Q}, q \neq p$. Thus, in any 2D plane defined by variables appearing in $\mathcal{C}$, with at least one variable appearing in $X$, the lines corresponding to $X = q$ and $X = p$ do not intersect. Consequently, in a plane where all the equations in $\mathcal{C}$ needed to derive $X = q$ and $X = p$ can be plotted, these lines must also not intersect. Therefore, we can explain $\mathcal{C} \to \perp$ by highlighting these contradictory equations in $\mathcal{C}$ and showing that their lines never intersect, regardless of variable assignments.

Figures 2 and 3 show examples of $\mathcal{D}_{\mathbb{Q},\text{lin}}$ explanations in EVONNE. The system of equations is shown in the top left. Hovering over an equation highlights its corresponding line in the 2D plot, and vice versa, helping users connect the algebraic and geometric views of the constraints. In Fig. 2 the top right displays an instantiation of the system’s solution based on the chosen value for the free variable. Since this system has one degree of freedom, setting $x_4 = 0$ uniquely determines the remaining variables. Hovering over the question mark icon reveals the solution without the variable assignment. In contrast, in Fig. 3, the top right shows the system of equations with respect to the currently chosen variable assignment. Additionally, users can manipulate the visualization directly by switching between different planes and assigning values to (free) variables using the controls beside the plot. In the case of unsatisfiability, the visualization makes contradictions immediately apparent: if a user assigns a value that causes an equation to evaluate to $p = q$ with $p \neq q$, then this inconsistency is highlighted in red, as illustrated by $3 = 0$ in Fig. 3.
<figure><img src="image_8.png" /><figcaption>Fig. 3. DQlin implication of ⊥ in EVONNE</figcaption></figure>

## 4.2 Explanations of $\mathcal{D}_{\mathbb{Q},\text{diff}}$ Entailments

It is well established that difference constraints (i.e., $x-y \le q$) can be represented as graphs such that every variable corresponds to a vertex and every constraint to a weighted edge [14]. Given a set of difference constraints, deciding whether it is unsatisfiable can be reduced to finding a simple cycle in the corresponding graph with a negative weight [14]. Therefore, we use graphs and negative cycles to explain implications in $\mathcal{D}_{\mathbb{Q},\text{diff}}$. However, since predicates in $\mathcal{D}_{\mathbb{Q},\text{diff}}$ express more types of constraints, we first need to introduce some necessary transformations.

Let $\mathcal{C}$ be a set of difference constraints. A difference graph is a weighted directed graph $G = (V, E)$, where each variable $x_i$ in $\mathcal{C}$ corresponds to a vertex $v_i \in V$, and each constraint $x_j - x_i \le q_{ij}$ corresponds to an edge $(v_i, v_j) \in E$ with weight $q_{ij} \in \mathbb{Q}$. A path $\pi(v, u)$ from $v$ to $u$ is a sequence of edges:

$$v \xrightarrow{q_0} v_1 \xrightarrow{q_1} v_2 \dots v_n \xrightarrow{q_n} u,$$

with weight $\pi^w(v, u) = q_0 + q_1 + \dots + q_n$. A path is simple if all vertices, with the possible exception of $v$ and $u$, are distinct. A negative cycle is a simple path $\pi(v, v)$ where $\pi^w(v, v) < 0$. A set of difference constraints is unsatisfiable iff the corresponding difference graph contains a negative cycle ([14, Theorem 24.9]).

Constraints in $\mathcal{D}_{\mathbb{Q},\text{diff}}$ of the form $y-x = q$ can be rewritten as two difference constraints: $y-x \le q$ and $x-y \le -q$. Additionally, the unary $\mathcal{D}_{\mathbb{Q},\text{diff}}$ constraints, i.e., constraints of the form $x \bowtie q$, where $\bowtie \in \{=, >\}$, can be represented as $x - z_0 \bowtie q$ where $z_0$ is a fresh variable. This formulation is sound because $x \bowtie q$ is satisfiable iff $\{x - z_0 \bowtie q, z_0 = 0\}$ is satisfiable ([14, Lemma 24.8]).

Lastly, we rewrite $x - z_0 > q$ as $z_0 - x \le -q - \epsilon$, where $\epsilon$ is a placeholder for some small positive value. This rewriting is sound for the following reason:
<figure><img src="image_9.png" /><figcaption>Fig. 4. Example of an explanation for $\mathcal{D}_{\mathbb{Q},\text{diff}}$ implications in EVONNE.</figcaption></figure>

If $\mathcal{C}$ is satisfiable and $\mathcal{C} \cup \{x - z_0 > q\}$ is unsatisfiable, then for any positive $e \in \mathbb{Q}$, the constraints $\mathcal{C} \cup \{x - z_0 \ge q + e\}$ are also unsatisfiable, which is equivalent to $\mathcal{C} \cup \{z_0 - x \le -q - e\}$. Meanwhile, for any assignment satisfying $\mathcal{C} \cup \{x - z_0 > q\}$, there exists a positive $e \in \mathbb{Q}$ such that the same assignment also satisfies $x - z_0 \ge q + e > q$. Thus, $\mathcal{C} \cup \{z_0 - x \le -q - e\}$ is also satisfiable. Since such a small positive rational number $e$ can always be found, we use $\epsilon$ symbolically as a reference to $e$ whenever we need to transform a constraint with a $>$-predicate, rather than computing the specific value $e$ for each set of constraints.

Consequently, we can represent any set $\mathcal{C}$ of $\mathcal{D}_{\mathbb{Q},\text{diff}}$ constraints as a difference graph, and if $\mathcal{C} \to \perp$, we can explain the contradiction in $\mathcal{C}$ by identifying the negative cycle in the graph. However, if $\mathcal{C}$ is satisfiable and $\mathcal{C} \to \beta$, an additional step is required. In particular, we can explain that $\mathcal{C}$ implies $\beta$ by showing that $\mathcal{C} \cup \{\neg \beta\} \to \perp$, which allows us to effectively use the notion of negative cycles to explain the implication. If $\beta$ is of the form $x > q$, then the negative cycle in the difference graph corresponding to $\mathcal{C} \cup \{x - z_0 \le q\}$ shows that whenever an assignment satisfies all the constraints in $\mathcal{C}$, the value of $x$ must be greater than $q$. If $\beta$ is of the form $x + y = q$, then $x + y \neq q$ is transformed into $x - y \le q - \epsilon \lor y - x \le -q - \epsilon$, leading to two negative cycles in the graph corresponding to $\mathcal{C} \cup \{x - y \neq q\}$. These cycles explain $\mathcal{C} \to x - y = q$ by demonstrating that no satisfying assignment for $\mathcal{C}$ exists unless $x - y = q$ holds.

Figure 4 shows an example of a negative cycle in EVONNE. Hovering over a constraint highlights its corresponding edge(s) in the graph, and vice versa. The dotted edges represent the negated conclusion. Furthermore, the negative cycle is animated, allowing users to visually follow its progression. This animation can be triggered by clicking on a vertex or a constraint; the clicked element then determines the starting point of the animation in the graph. Additionally,
<figure><img src="image_10.png" /><figcaption>Fig. 5. Popover for specifying new project information in EVONNE.</figcaption></figure>

users have access to a feature that lets them assign concrete values to variables by double-clicking on them. These values are then automatically propagated along the negative cycle, allowing users to observe how the set of constraints behaves under such assignments. In particular, this makes it possible to see exactly how the cycle leads to logical inconsistencies, which are highlighted in red. An example of such a contradiction is $x_3 = 3 \le 3 - \epsilon$, as shown in Fig. 4.

# 5 Numerical Explanations in EVONNE

The first step to using EVONNE to generate CD explanations is to create a new project. As shown in Fig. 5, users must first specify which reasoner they would like to use—which, in our case, is the CD reasoner. This selection prompts the user to choose one of the two supported domains. Since the OWL 2 standard [28] does not support all predicate types used in our concrete domains, EVONNE requires the user to provide two files for an ontology: one text file that contains the CD constraints of the ontology, and one OWL file that contains the DL part. Once the files are loaded, the user is asked to provide an axiom (concept inclusion) that they would like to have proven. If proving this axiom depends on the concrete domain part of the ontology, then a combined proof is generated and displayed.

By default, all numerical subproofs within a combined proof are collapsed into single inferences. Each of these inferences is labeled with a unique rule identifier—for example, the label CDP1 used in the proof shown in Fig. 1a—which allows for a more compact presentation of the proof. However, users can expand these subproofs to reveal all intermediate inferences. The visual explanations are accessible by clicking the labels of the numerical subproofs, which appear as popovers, as shown in Figs. 2, 3, and 4). It is worth noting that visual
explanations rely only on the constraints within the corresponding subproofs and do not use additional constraints from the ontology.

The CD explanations in EVONNE use *function-plot* and *cytoscape.js* to render the 2D plots and difference graphs, respectively. To handle numerical precision in JavaScript, we represent rational numbers as fractions, using *Fraction.js*. We implemented a Gaussian elimination solver for evaluating $D_{Q,lin}$ equations, and a Hamiltonian cycle detector for animating the negative cycles. In our difference graphs, a negative-weight Hamiltonian cycle is guaranteed. This is because our graphs are based on minimal proofs, ensuring that (i) all necessary constraints for constructing the negative cycle are present, and (ii) no constraint is superfluous, as the proof's leaf constraints correspond to a justification, i.e., a minimal set of constraints entailing the proof's root constraint [3].

The current version of EVONNE is accessible through https://imld.de/evonne, where all the examples used in the user studies (Sect. 6.1) and the benchmark (Sect. 6.2) are listed under the *Play Around* tab of EVONNE.

# 6 Evaluation

We conducted two experiments to evaluate different aspects of our approach. The first experiment consists of user studies that assess the effectiveness of the numerical explanations in terms of user understanding and perceived helpfulness. The second experiment is a benchmark that evaluates the efficiency of rendering these explanations.

## 6.1 User Studies

To assess the CD explanations we conducted two qualitative studies—one for $D_{Q,diff}$ and the other for $D_{Q,lin}$—using online structured interviews. Both studies compared the classical proofs (e.g., Figs. 1b, and 1c) with their respective alternative CD explanation (e.g., Figs. 2, 3, 4). The goal was to compare the effectiveness of the explanations and collect feedback to improve them.

To ensure adherence to best scientific practices, we preregistered the studies. The preregistration, an extended report, and detailed user feedback are available online [20].

*Study Design.* We employed a 2x2 factorial design with two independent variables: **representation** (i.e., *plot/cycle* or *proof*), and **task type** (i.e., *unsatisfiability* or *entailment*). The task type condition was necessary due to slight differences in plot and cycle representations between cases. Within each domain, four visual explanations of comparable difficulty were created with EVONNE. Each task in $D_{Q,lin}$ involved 3-4 linear equations and, for $D_{Q,diff}$, 4-6 difference constraints. We used a within-subjects design with a randomized order: all participants experienced all conditions and examples. The dependent variables included ease of use (measured using Single Ease Question, SEQ [24]), user experience (assessed with User Experience Questionnaire, UEQ-S [21,26]),
<figure><img src="image_11.png" /><figcaption>**Fig. 6.** Distribution of SEQ responses in *D*<sub>Q,diff</sub>: X-axis represents how difficult it was to understand an explanation, and Y-axis indicates the number of participants who selected each class.</figcaption></figure>

and subjective preference. These dependent variables are interrelated. As demonstrated further, subjective preferences consistently aligned with the results from SEQ and UEQ-S, reinforcing the validity of our findings. The online surveys were hosted on LimeSurvey [1] and included an introductory video for each domain. The *D*<sub>Q,diff</sub> study averaged just 35 minutes, whereas the *D*<sub>Q,lin</sub> study required an average of 50 minutes.

We recruited eleven participants (2 female, 9 male), aged 18–44, from among colleagues familiar with logic and linear algebra, of whom seven were Ph.D.s, two M.Sc.s, and one B.Sc. Participants were informed about the objective of the studies and consented to the use of anonymous data for scientific purposes.

**Results for** $D_{Q,diff}$. First, SEQ shows how difficult the explanation is to understand on a Likert scale from 1 “very difficult” to 7 “very easy”. Figure 6 demonstrates the following findings: For an *entailment* task, *cycles* and *proofs* received similar evaluations (*cycles*: average 5.6, sd. = 0.9; *proofs*: average 5.8, sd. = 1.2, respectively). However, for *unsatisfiability*, *cycles* received an average score of 6, sd. = 0.8, and were unanimously perceived as more intuitive than *proofs* (average 5, sd. = 1.3).

In addition to SEQ, participants briefly explained why they found a task difficult. They generally found *cycles* and their animations clear and understandable, particularly because the visualization automated calculations, highlighted negative cycles, and helped relate edges to constraints. However, a few participants noted that understanding the interface and interpreting the information required some initial effort, explanations, and practice, as in “*It took me a moment to understand the tool. Once I was given the explanation, I could understand how it works*”. On the other hand, *proofs* were perceived slightly less positively. While participants appreciated the ability to inspect inference steps, clearly identify which equations to combine, and the simplicity of step verification, they also noted some challenges. These included uninformative or redundant information (e.g., repetitive left-hand sides of axioms and overly lengthy node labels), the need for manual calculations, and difficulties with the semantics of edge opera-
<figure><img src="image_12.png" /><figcaption>**Fig. 7.** $D_{Q,lin}$ proof (in blue), plot (in cyan), $D_{Q,diff}$ proof (in white), and cycle (in gray) UEQ-S scores, their interpretation, and confidence intervals. (Color figure online)</figcaption></figure>

tions. For instance, a participant remarked: *“Proofs take a lot of space, and the edge labelings are unfamiliar”*.

Overall, both methods were well received, with participants appreciating their different strengths. As one participant summarized: *“A positive implication is actually very well represented in a proof. Cycle highlighting, hovering and animation are super cool”*.

Next, we assessed the user experience using the UEQ-S [25], by calculating *pragmatic* and *hedonic* quality scores. Pragmatic usability focuses on the task-oriented nature of an experience, whereas hedonic usability reflects non-utilitarian aspects such as appeal, originality, and joy of use. The white and gray bars in Fig. 7 correspond to the following results: *Proofs* received an “above average” rating across all qualities, with scores of 1.364 (pragmatic quality, e.g., usability and functionality), 1 (hedonic quality, e.g., enjoyment and stimulation), and 1.182 (overall quality). In contrast, *cycles* were rated as “excellent” in all three categories, with scores of 1.795 (pragmatic), 1.727 (hedonic), and 1.761 (overall).

After each task, participants were asked whether the explanation service was useful for understanding. All but one participant responded “yes” across both task types and both representations. The outlier cited confusion related to the naming of *proof* edges.

Finally, in the post-test assessment in $D_{Q,diff}$, most participants preferred *cycles* (8 vs. 2 for *proofs*, 1 for both). This preference grew stronger with more constraints (9 vs. 2 for *proofs*).
<figure><img src="image_13.png" /><figcaption>**Fig. 8.** Distribution of SEQ responses in *D*<sub>Q,lin</sub>: The X-axis represents how difficult it was to understand an explanation, and the Y-axis indicates the number of participants who selected each class.</figcaption></figure>

**Results for** D<sub>Q,lin</sub>. Regarding SEQ, Fig. 8 demonstrates that, across both task types—*unsatisfiability* and *entailment*—*plots* (with average scores of 4.7, sd. = 2.2, and 3.9, sd. = 1.8, respectively) were perceived as less intuitive than *proofs* (with average scores of 5.3, sd. = 1.2, and 4.8, sd. = 1.5, respectively). In the case of *plots*, participants found them useful and enjoyable but also cognitively demanding to combine and interpret multiple variables displayed simultaneously, in particular when dealing with a higher number of dimensions. A respondent highlighted this point: *“The projection made me think that the solution was a point at first, before I realized that the solution is higher dimensional.”*. Unsatisfiability tasks are perceived slightly easier than the *entailment* ones. Over time, familiarity with the visualization also improved, aided by provided instructions. For *proofs*, some participants found the step-by-step approach helpful, as it made the task easier to follow and verify compared to *plots*. They appreciated the ability to trace each step and felt confident in the overall result due to its clear mathematical foundation. However, the mental calculations required for verifying were quite challenging, as one participant noted: *“For proofs, I like that they show each individual step, but I did not figure out the solution myself from proofs, instead I trusted the system.”*. Many participants found the notation less accessible, in particular: *“Too many symbols and too long node labels so it was hard to parse.”*

With respect to user experience, the blue and cyan bars in Fig. 7 illustrate the following findings: *Proofs* received an overall rating of “above average” (1.159). Specifically, they scored “above average” (1.523) for pragmatic qualities (e.g., usability and functionality) but “below average” (0.795) for hedonic qualities (e.g., enjoyment and stimulation). In contrast, *plots* were rated overall as “below average” (0.795). They scored “bad” (0.568) for pragmatic qualities but achieved an “above average” (1.023) rating for hedonic qualities.

After each task, we asked if the explanation was helpful. For *proofs*, the response was unanimously positive across both task types. Feedback on *plots*
varied: for *unsatisfiability*, 10 said “yes” and 1 was “not sure”; for *entailment*, 6 said “yes”, 4 were “not sure”, and 1 said “no”.

Subjectively, most participants preferred *proofs* (8 vs. 2 for *plots*, 1 for both). However, when linear equations involved only 2–3 variables, preference shifted to *plots* (8 vs. 3 for *proofs*).

**Discussion.** The user studies demonstrate that concrete domain-specific visualizations can significantly enhance the understanding of numerical reasoning, especially in the case of *D<sub>Q,diff</sub>*, where animated cycles were preferred for their clarity and intuitiveness. While proof trees were appreciated for their structure and detail, the choice between concrete domain visualizations and proofs appears task-dependent and influenced by numerical complexity. For simpler *D<sub>Q,lin</sub>* entailments involving few variables, users preferred plots; however, for more complex cases and even with the added cognitive load, proofs were still preferred, as they were perceived as more trustworthy. These insights suggest that offering multiple, complementary explanation forms—proofs and CD visualizations—can accommodate diverse user preferences and experience levels. Future iterations of EVONNE could build on this by incorporating adaptive explanation strategies based on characteristics of entailments or user feedback. Additionally, enabling users to adjust the existing visual explanations—or even extend them with user-defined visualizations, as supported by systems like Sterling [17]—could further accommodate individual preferences.

## 6.2 Performance Benchmark

We measured the response times for rendering the concrete domain explanations using combined proofs from the dataset provided in [5]. To automate the process, we used cypress.io, a testing framework, to load these proofs and open the corresponding CD explanations. Since the goal of the benchmark is to assess the rendering overhead introduced by the visual explanations, we do not measure the time required to compute the combined proofs, as this has already been reported in [6].

On average, response times were 18.32 ms for *D<sub>Q,lin</sub>* and 8.7 ms for *D<sub>Q,diff</sub>*. The slowest times were 180.4 ms for *D<sub>Q,lin</sub>* and 124.8 ms for *D<sub>Q,diff</sub>*, which correspond to large proofs that push the browser’s resources considerably. These higher initial times occur when a CD explanation is opened for the first time, as the required HTML DOM elements are created and the relevant libraries are loaded. However, subsequent renders within the same proof are significantly faster. In the slowest cases, follow-up renders took 44.4 ms in *D<sub>Q,lin</sub>* and 9.3 ms in *D<sub>Q,diff</sub>*. Note that all response times are within the 200ms threshold for perceived responsiveness [16].

## 7 Conclusion

We have extended EVONNE to generate and present proofs for *EL<sub>⊥</sub>[D<sub>Q,diff</sub>] and *EL<sub>⊥</sub>[D<sub>Q,lin</sub>]. Additionally, we have designed and developed alternative visual
explanations for numerical entailments, taking into account the characteristics of each concrete domain. Specifically, we illustrate $\mathcal{D}_{\mathbb{Q},\text{diff}}$ entailments using negative cycles and $\mathcal{D}_{\mathbb{Q},\text{lin}}$ entailments with 2D plots. These visual explanations are specific to the concrete domain yet independent of the underlying logic, making them adaptable and applicable to other formalisms. Furthermore, the visual display of the CD explanations scales better than that of the combined proofs. For instance, in the case of $\mathcal{D}_{\mathbb{Q},\text{lin}}$, adding more constraints simply results in additional lines in a 2D plot, without significantly affecting the overall layout. In contrast, increasing the number of equations in a proof expands the entire proof structure, which can make navigation more difficult due to increased scrolling and zooming.

We conducted qualitative user studies to assess the effectiveness of numerical explanations in EVONNE. For $\mathcal{D}_{\mathbb{Q},\text{lin}}$, participants' opinions varied, though most alluded to a trust factor favoring proofs over visual explanations, suggesting that, in this case, such visual explanations might not be necessary. In contrast, for $\mathcal{D}_{\mathbb{Q},\text{diff}}$, participants highly valued the clarity and ease of understanding provided by the animated cycles, making them a more preferred form of explanation.

As future work, we plan to address issues raised by the participants' feedback on both proofs and the visual CD explanations. Additionally, we will refine EVONNE's capabilities for explaining non-consequences through counter-interpretations and extend them to support DLs with concrete domains.

**Acknowledgments.** This work is funded by Deutsche Forschungsgemeinschaft (DFG) under Germany's Excellence Strategy: EXC 2050/1, 390696704 – "Centre for Tac-tile Internet" (CeTI); by DFG grant 389792660 as part of TRR 248 – CPEC, see https://perspicuous-computing.science; and by Bundesministerium für Bildung und Forschung (BMBF) and Saxon State Ministry for Science, Culture and Tourism (SMWK) in Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI, SCADS22B). The authors extend gratitude to Dr. Ida Sri Rejeki Siahaan and Nicolás Rojas for their support in the early design and implementation of CD visualizations.

## References

1. Der Umfragedienst für sächsische Hochschulen und Berufsakademien. https://bildungsportal.sachsen.de/umfragen/

2. Alrabbaa, C., Baader, F., Borgwardt, S., Dachselt, R., Koopmann, P., Méndez, J.: Evonne: interactive proof visualization for description logics (system description). In: Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 271–280. Springer (2022). https://doi.org/10.1007/978-3-031-10769-6_16

3. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding small proofs for description logic entailments: theory and practice. In: LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020. EPiC Series in Computing, vol. 73, pp. 32–67. EasyChair (2020). https://doi.org/10.29007/NHPP
4. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding good proofs for description logic entailments using recursive quality measures. In: Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction 2021, Proceedings. Lecture Notes in Computer Science, vol. 12699, pp. 291-308. Springer (2021). https://doi.org/10.1007/978-3-030-79876-5_17

5. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Combining proofs for description logic and concrete domain reasoning. In: Rules and Reasoning - 7th International Joint Conference, RuleML+RR 2023, Proceedings. Lecture Notes in Computer Science, vol. 14244, pp. 54-69. Springer (2023). https://doi.org/10.1007/978-3-031-45072-3_4

6. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Combining proofs for description logic and concrete domain reasoning (technical report) (2023). https://arxiv.org/abs/2308.03705

7. Alrabbaa, C., et al.: Explaining reasoning results for OWL ontologies with Evee. In: Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam. November 2-8, 2024 (2024). https://doi.org/10.24963/KR.2024/67

8. Alrabbaa, C., Hieke, W.: Explaining non-entailment by model transformation for the description logic *EL*. In: Proceedings of the 11th International Joint Conference on Knowledge Graphs, IJCKG 2022, pp. 1-9. ACM (2022). https://doi.org/10.1145/3579051.3579060

9. Alrabbaa, C., Hieke, W., Turhan, A.: Counter model transformation for explaining non-subsumption in *EL*. In: Proceedings of the 7th Workshop on Formal and Cognitive Reasoning co-located with the 44th German Conference on Artificial Intelligence (KI 2021). CEUR Workshop Proceedings, vol. 2961, pp. 9-22. CEUR-WS.org (2021). https://ceur-ws.org/Vol-2961/paper_2.pdf

10. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005. pp. 364-369. Professional Book Center (2005). http://ijcai.org/Proceedings/05/Papers/0372.pdf

11. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24-30, 1991, pp. 452-457. Morgan Kaufmann (1991). http://ijcai.org/Proceedings/91-1/Papers/070.pdf

12. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge Univ. Press (2017). https://doi.org/10.1017/9781139025355

13. Baader, F., Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. J. Autom. Reason. **66**(3), 357-407 (2022). https://doi.org/10.1007/s10817-022-09626-2

14. Cormen, T., Leiserson, C., Rivest, R., Stein, C.: Introduction to Algorithms, third edition. Computer science, MIT Press (2009). https://books.google.de/books?id=i-bUBQAAQBAJ

15. Cunningham, J.P., Ghahramani, Z.: Linear dimensionality reduction: survey, insights, and generalizations. J. Mach. Learn. Res. **16**, 2859-2900 (2015). https://doi.org/10.5555/2789272.2912091

16. Dabrowski, J.R., Munson, E.V.: Is 100 milliseconds too fast? In: CHI 2001 Extended Abstracts on Human Factors in Computing Systems, CHI Extended Abstracts 2001, Seattle, Washington, USA, March 31 - April 5, 2001. pp. 317-318. ACM (2001). https://doi.org/10.1145/634067.634255
17. Dyer, T., Jr., J.W.B.: Sterling: a web-based visualizer for relational modeling languages. In: Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12709, pp. 99-104. Springer (2021). https://doi.org/10.1007/978-3-030-77543-8_7

18. Gunning, D., Stefik, M., Choi, J., Miller, T., Stumpf, S., Yang, G.: XAI – explainable artificial intelligence. Sci. Robotics 4(37) (2019). https://doi.org/10.1126/SCIROBOTICS.AAY7120

19. Holzinger, A., Saranti, A., Molnar, C., Biecek, P., Samek, W.: Explainable AI methods - a brief overview. In: xxAI – Beyond Explainable AI - International Workshop, Held in Conjunction with ICML 2020, Revised and Extended Papers. Lecture Notes in Computer Science, vol. 13200, pp. 13-38. Springer (2020). https://doi.org/10.1007/978-3-031-04083-2_2

20. Kovtunova, A., Alrabbaa, C., Baader, F., Dachselt, R., Méndez, J.: The Concrete Evonne (2025). https://doi.org/10.17605/OSF.IO/Y4X5T

21. Laugwitz, B., Held, T., Schrepp, M.: Construction and evaluation of a user experience questionnaire. In: HCI and Usability for Education and Work, 4th Symposium of the Workgroup Human-Computer Interaction and Usability Engineering of the Austrian Computer Society, USAB 2008, Graz, Austria, November 20-21, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5298, pp. 63-76. Springer (2008). https://doi.org/10.1007/978-3-540-89350-9_6

22. Lutz, C.: Description logics with concrete domains-a survey. In: Advances in Modal Logic 4, papers from the fourth conference on "Advances in Modal logic," held in Toulouse, France, 30 September - 2 October 2002, pp. 265-296. King's College Publications (2002). http://www.aiml.net/volumes/volume4/Lutz.ps

23. Méndez, J., Alrabbaa, C., Koopmann, P., Langner, R., Baader, F., Dachselt, R.: Evonne: A visual tool for explaining reasoning with OWL ontologies and supporting interactive debugging. Comput. Graph. Forum 42(6) (2023). https://doi.org/10.1111/CGF.14730

24. Sauro, J., Dumas, J.S.: Comparison of three one-question, post-task usability questionnaires. In: Proceedings of the 27th International Conference on Human Factors in Computing Systems, CHI 2009, Boston, MA, USA, April 4-9, 2009 pp. 1599-1608. ACM (2009). https://doi.org/10.1145/1518701.1518946

25. Schrepp, M.: User Experience Questionnaire Handbook (2015). https://doi.org/10.13140/RG.2.1.2815.0245

26. Schrepp, M., Hinderks, A., Thomaschewski, J.: Design and evaluation of a short version of the user experience questionnaire (UEQ-S). Int. J. Interact. Multim. Artif. Intell. 4(6), 103-108 (2017). https://doi.org/10.9781/IJIMAI.2017.09.001

27. Søgaard, A.: On the opacity of deep neural networks. Can. J. Philos. 53(3), 224-239 (2023). https://doi.org/10.1017/can.2024.1

28. W3C OWL Working Group: OWL 2 Web Ontology Language Document Overview (Second Edition) - W3C Recommendation 11 December 2012 (2012). http://www.w3.org/TR/owl2-overview/
**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_14.png" /></figure>
# The Expressive Power of Description Logics with Numerical Constraints over Restricted Classes of Models

Franz Baader<fnref n="1" />,<fnref n="2" /> ID and Filippo De Bortoli<fnref n="1" />,<fnref n="2" />(✉) ID

**Abstract.** Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in *ALCSCC*, while the comparison of feature values of different individuals in *ALC(Ξ)* has been studied in the context of *ω*-admissible concrete domains *Ξ*. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL *ALCOSCC(Ξ)*, which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of *Ξ* is also decidable in exponential time. It is thus not higher than the complexity of the basic DL *ALC*. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.

## 1 Introduction

*Description logics* (DLs) [6,13] are a prominent family of logic-based knowledge representation languages, which can be used to formalize the terminological knowledge of an application domain in a machine-processable way. For instance, the standard Web Ontology Language OWL<fnref n="1" /> is based on an expressive DL and the large medical ontology SNOMED CT<fnref n="2" /> has been developed using a rather inexpressive DL. The *expressive power* of a DL is determined by the constructors that are available for building complex concept descriptions out of concept

<footnote n="1">¹ Institute of Theoretical Computer Science, TU Dresden, Dresden, Germany
franz.baader@tu-dresden.de</footnote>

<footnote n="2">² Center for Scalable Data Analytics and AI (ScaDS.AI), Dresden/Leipzig, Germany
filippo.de_bortoli@tu-dresden.de</footnote>

<footnote n="1">¹ https://www.w3.org/TR/owl2-overview/.</footnote>

<footnote n="2">² https://www.snomed.org/.</footnote>
names (unary predicates) and role names (binary predicates). For example, the concept description Person $\sqcap \exists$pet.Dog, describing persons that have a dog as a pet, uses conjunction ($\sqcap$) and existential restriction ($\exists r.C$) as constructors, where Person and Dog are concept names and pet is a role name. To show that a given DL $\mathcal{L}_1$ can be expressed by another DL $\mathcal{L}_2$ using the same concept and role names, we can provide a semantic-preserving translation of $\mathcal{L}_1$ concept descriptions into $\mathcal{L}_2$ concept descriptions. Proving inexpressivity is more challenging. The first formal investigation of the expressive power of DLs was performed in [1,2], but in a rather ad hoc manner. More fundamental characterizations of the expressive power of various concept description languages up to the DL $\mathcal{ALC}$ based on the model-theoretic notion of bisimulation are given in [20]. Basically, this approach (pioneered by van Benthem [28] for the modal logic K, which is a syntactic variant of $\mathcal{ALC}$) characterizes a given DL as the fragment of first-order logic (FOL) that is invariant under an appropriate notion of bisimulation.

The expressive power of $\mathcal{ALC}$ can, for instance, be extended by enabling the use of numerical constraints within concept descriptions. In the extension $\mathcal{ALCQ}$ of $\mathcal{ALC}$, qualified number restrictions [18] can be employed to constrain the number of role successors belonging to a certain concept; e.g., Person $\sqcap (\ge 3 \text{ child.Female}) \sqcap (\le 2 \text{ pet.Dog})$ describes persons that have at least 3 daughters and at most 2 dogs as pets. The DL $\mathcal{ALCSCC}$ [3] extends $\mathcal{ALCQ}$ with very expressive counting constraints on role successors expressed in the logic QFBAPA [19]. Since QFBAPA only considers finite sets and their cardinalities, the semantics of $\mathcal{ALCSCC}$ is restricted to finitely branching interpretations, where each element can have only finitely many role successors. In $\mathcal{ALCSCC}$ one can, e.g., describe persons that have more daughters than they have dogs as pets, without using specific numbers as upper/lower bounds for the numbers of pet dogs and daughters. Bisimulation-based characterizations of $\mathcal{ALCQ}$ (or its modal logic variant of K extended with graded modalities) can be found in [22,25,26]. In [7,8], we have investigated the expressivity of DLs with expressive counting constraints. However, to dispense with the requirement that interpretations be finitely branching, we used an infinite variant $\text{QFBAPA}^\infty$ of QFBAPA to formulate these constraints, which yields the variant $\mathcal{ALCSCC}^\infty$ of $\mathcal{ALCSCC}$. We were able to show that $\mathcal{ALCSCC}^\infty$ is not a fragment of FOL and characterized the first-order fragment of this logic ($\mathcal{ALCCQU}$ or equivalently $\mathcal{ALCQt}$) using a form of counting bisimulation [22]. The first major contribution of the present paper is to prove the same results for $\mathcal{ALCSCC}$, where only finitely branching interpretations are available. The proof techniques used in [7,8], which were inspired by the ones in [22], cannot be employed in this setting since they depend on compactness of FOL, which does not hold for the restriction of FOL to finitely branching interpretations. Instead, we employ a proof technique inspired by [25,27], which utilizes locality properties of FOL rather than compactness. Interestingly, this approach can deal with arbitrary interpretations, finitely branching interpretations, and finite interpretations in a uniform way.

An orthogonal approach for employing numerical constraints within concept descriptions is the use of numerical concrete domains [14,21]. In a DL with a
concrete domain, concrete objects such as numbers or strings can be assigned
to individuals using partial functions called *features*. For example, the concept
description Person $\sqcap \exists$ child age, pet age. < describes persons that have a child that
is younger than one of their pets. Here, *age* is a feature that assigns a rational
number, their age, to some of the elements of the interpretation domain, and <
is the usual smaller relation between rational numbers. In [9, 10], we have inves-
tigated the abstract expressive power of DLs with concrete domains, which only
considers the abstract part of interpretations, i.e., ignores the values assigned
to features. We have shown that the abstract expressive power of $\mathcal{ALC}(\mathfrak{D})$, i.e.,
$\mathcal{ALC}$ extended with the concrete domains $\mathfrak{D}$, is contained in FOL for certain
concrete domains, but have also exhibited a large class of concrete domains for
which this is not the case. The *second major contribution* of the present paper
is to introduce a notion of concrete expressive power for DLs with concrete
domains that also takes the feature values into account. For example, if we take
two concrete domains over the rational numbers, where one has as only pred-
icate $+_1$ (relating $q \in \mathbb{Q}$ with $q + 1$) and the other $+_2$ (relating $q \in \mathbb{Q}$ with
$q + 2$), then the extensions of $\mathcal{ALC}$ with these concrete domains have the same
abstract expressive power, but their concrete expressive power is incomparable.
Using proof techniques similar to the ones employed for $\mathcal{ALCSCC}$ we can charac-
terize $\mathcal{ALC}(\mathfrak{D})$ as the fragment of FOL($\mathfrak{D}$) (i.e., FOL extended with the concrete
domain $\mathfrak{D}$) that is invariant under an appropriate notion of bisimulation.

A technical report containing detailed proofs of all the results introduced in
this paper is available online [11].

## 2 Preliminaries

We start by introducing the base logic $\mathcal{ALC}$ before defining its two orthogonal
extensions with numerical constraints. Since here we focus on the expressivity
of concept description languages, we do not introduce TBoxes, ABoxes, or rea-
soning problems (see [13] for more details on $\mathcal{ALC}$ and other classical DLs).

**The classical DL ALC** Given disjoint, at most countable sets $N_C$ and $N_R$ of concept and role names, *ALC* concept descriptions (*concepts* for short) are built from concept names using negation (`$\neg C$`), conjunction (`$C \sqcap D$`), and existential restrictions (`$\exists r.C$`), where $r \in N_R$ and $C, D$ are *ALC* concept descriptions. As usual, we define $C \sqcup D := \neg(\neg C \sqcap \neg D)$ (disjunction), $\forall r.C := \neg\exists r.\neg C$ (value restriction) and $\top := A \sqcup \neg A$ (top concept). An interpretation $I$ consists of a non-empty domain $\Delta^I$ and a mapping $.^I$ assigning a set $A^I \subseteq \Delta^I$ to $A \in N_C$ and a binary relation $r^I \subseteq \Delta^I \times \Delta^I$ to $r \in N_R$. For $d \in \Delta^I$, we define $r^I(d) := \{e \in \Delta^I \mid (d, e) \in r^I\}$. We extend $.^I$ to concepts by `($\neg C$)^I := \Delta^I \setminus C^I$, `($C \sqcap D$)^I := C^I \cap D^I` and `($\exists r.C$)^I := \{d \in \Delta^I \mid r^I(d) \cap C^I \neq \emptyset\}`. In this DL, the concept of a person not having a dog as a pet can be written as `Person $\sqcap \forall$ pet. $\neg$ Dog`.

**The DL ALSCC** This DL employs the logic *QFBAPA* [19] to state cardinal-
ity constraints on role successors that are more expressive than existential and
value restrictions. In QFBAPA, *set terms* are built from *set variables* and the
constants $\emptyset$ and $\mathcal{U}$ using intersection $\cap$, union $\cup$ and complement $^c$. A QFBAPA formula is a Boolean combination of atomic formulae of the form

$$m_0 + m_1|s_1| + \cdots + m_k|s_k| \le n_0 + n_1|t_1| + \cdots + n_\ell|t_\ell| \quad (1)$$

where each $s_i$, $t_j$ is a set term and each $m_i$, $n_j$ is a natural number.<fnref n="3" /> A solution $\sigma$ of a QFBAPA formula $\phi$ assigns a finite set $\sigma(\mathcal{U})$ to $\mathcal{U}$, the empty set to $\emptyset$ and subsets of $\sigma(\mathcal{U})$ to set variables such that $\phi$ is satisfied by $\sigma$, in the standard way. Checking if a QFBAPA formula has a solution is an NP-complete problem [19]. The logic QFBAPA$^\infty$ [7] has the same syntax as QFBAPA, but solutions may assign infinite sets to $\mathcal{U}$. Its satisfiability problem is also NP-complete [7].

ALCSCC extends the syntax of ALC with the new constructor role successor restriction (or succ-restriction) succ(con), where con is an atomic QFBAPA formula with role names and ALCSCC concept descriptions as set variables [3]. For instance, the concept of all persons that have more daughters than they have dogs as pets can be expressed in ALCSCC as succ(|pet $\cap$ Dog| < |child $\cap$ Female|). Note that existential restrictions $\exists r.C$ are not needed as explicit constructors in this DL since they can be expressed as succ(|r $\cap$ C| $\ge$ 1).

When defining the semantics of ALCSCC, interpretations $\mathcal{I}$ are required in [3] to be finitely branching, i.e. such that the set of all role successors $\mathcal{I}^r(d) := \bigcup_{r \in N_R} r^\mathcal{I}(d)$ is finite, for all $d \in \Delta^\mathcal{I}$. Then, each $d \in \Delta^\mathcal{I}$ induces a QFBAPA assignment $\sigma_d$, where $\sigma_d(\mathcal{U}) := \mathcal{I}^r(d)$, $\sigma_d(r) := r^\mathcal{I}(d)$ for $r \in N_R$ and $\sigma_d(C) := C^\mathcal{I} \cap \mathcal{I}^r(d)$ for concepts $C$. The mapping $\cdot^\mathcal{I}$ is extended to succ-restrictions by defining $d \in succ(con)^\mathcal{I}$ iff $\sigma_d$ is a solution of con.

The DL ALCSCC$^\infty$ is defined in [7] with the same syntax as ALCSCC, but in the semantics arbitrary interpretations are allowed. Consequently, the assignment $\sigma_d$ may be such that $\sigma_d(\mathcal{U})$ is infinite, and thus satisfaction of the constraint con by $\sigma_d$ is evaluated in QFBAPA$^\infty$ rather than QFBAPA.

In the definitions of ALCSCC$^\infty$ and ALCSCC, we considered two classes of first-order interpretations: the class $C_{\text{all}}$ of all interpretations and the class $C_{\text{fb}}$ of finitely branching interpretations. Later on, we will also consider the class $C_{\text{fin}}$ of all finite interpretations, which is also of interest in DL research [17,23]. Our results on the expressive power will be parameterized with a class $C$ of interpretations satisfying certain restrictions. Since the syntax of ALCSCC$^\infty$ and ALCSCC coincide, we will in the following always talk about ALCSCC concepts. However, if $C$ contains interpretations that are not finitely branching, then the semantics uses QFBAPA$^\infty$ rather than QFBAPA.

**DLs with Concrete Domains.** Following [12,14,21], we use the term concrete domain to refer to a relational structure $\mathfrak{D} = (D, \dots, P^D, \dots)$ over a non-empty, at most countable relational signature, where $D$ is a non-empty set, and each predicate $P$ has an associated arity $k_P \in \mathbb{N}$ and is interpreted by a relation $P^D \subseteq D^{k_P}$. An example is the structure $\mathfrak{Q} := (\mathbb{Q}, <, =, >)$ over

<footnote n="3">³ Following [8], we use a streamlined definition of QFBAPA that does not explicitly introduce set constraints and divisibility constraints.</footnote>
the rational numbers $\mathbb{Q}$ with standard binary ordering and equality relations. Given a countable set $V$ of variables, a constraint system over $V$ is a set $\mathcal{C}$ of constraints $P(v_1, \dots, v_k)$, where $v_1, \dots, v_k \in V$ and $P$ is a $k$-ary predicate of $\mathcal{D}$. We denote by $V(\mathcal{C})$ the set of variables that occur in $\mathcal{C}$. The constraint system $\mathcal{C}$ is satisfiable if there is a mapping $h: V(\mathcal{C}) \to D$ such that $P(v_1, \dots, v_k) \in \mathcal{C}$ implies $(h(v_1), \dots, h(v_k)) \in P^D$. The constraint satisfaction problem for $\mathcal{D}$, denoted CSP($\mathcal{D}$), asks if a given finite constraint system $\mathcal{C}$ over $\mathcal{D}$ is satisfiable. The CSP of $\mathcal{D}$ is decidable in polynomial time, by reduction to $\langle - \rangle$-cycle detection: for example, the system $\{x_1 < x_2, x_2 < x_3, x_3 < x_1\}$ is unsatisfiable over $\mathcal{D}$.

When integrating such a concrete domain into the DL $\mathcal{ALC}$, it needs to satisfy certain restrictions to obtain a decidable DL. Without a TBox, admissibility is required in [12] whereas in the presence of a TBox the stronger $\omega$-admissibility is required in [14,21]. In the context of our investigation of the expressive power of DLs with concrete domains, it is sufficient to assume that negated constraints can be expressed using one or more non-negated ones.

**Definition 1.** A structure $\mathcal{D}$ is weakly closed under negation (WCUN) if for all $k \ge 1$ and all $k$-ary relations $P$ of $\mathcal{D}$ there are $k$-ary relations $P_1, \dots, P_{n_P}$ such that $(d_1, \dots, d_k) \notin P^D$ iff $(d_1, \dots, d_k) \in \bigcup_{i=1}^{n_P} P_i^D$ for all $d_1, \dots, d_k \in D^k$.

It is easy to see that both admissible and $\omega$-admissible concrete domains satisfy this property. Examples of $\omega$-admissible, and thus WCUN, concrete domains are Allen's interval algebra, RCC8 and $\mathcal{D}$ [14,21]. For example the negated predicate $\notin \mathcal{D}$ is obtained as the union of $<$ and $>$.

To integrate a given concrete domain $\mathcal{D}$ into $\mathcal{ALC}$, we complement $\mathbb{N}_C$ and $\mathbb{N}_R$ with a finite set $\mathbb{N}_F$ of feature names that connect individuals with values in $D$ [12]. A feature path $p$ is of the form $f$ or $rf$ with $r \in \mathbb{N}_R$ and $f \in \mathbb{N}_F$. For instance, age is a feature name as well as a feature path, while child age is a feature path including the role name child. The DL $\mathcal{ALC}(\mathcal{D})$ extends $\mathcal{ALC}$ with concrete domain restrictions (or CD-restrictions) of the form $\exists p_1, \dots, p_k.P$ and $\forall p_1, \dots, p_k.P$, where $p_i$ are feature paths and $P$ is a $k$-ary predicate of $\mathcal{D}$. An interpretation $\mathcal{I}$ assigns to $f \in \mathbb{N}_F$ a partial function $f^\mathcal{I}: \Delta^\mathcal{I} \to D$. A feature path $p$ is mapped to $p^\mathcal{I} \subseteq \Delta^\mathcal{I} \times D$ by defining$^4$ $p^\mathcal{I}(d) := \{f^\mathcal{I}(d)\}$ if $p = f$ and $p^\mathcal{I}(d) := \{f^\mathcal{I}(e) \mid e \in r^\mathcal{I}(d)\}$ if $p = rf$. Then we can define

$$ (\exists p_1, \dots, p_k.P)^\mathcal{I} := \{d \in \Delta^\mathcal{I} \mid \text{some tuple in } p_1^\mathcal{I}(d) \times \dots \times p_k^\mathcal{I}(d) \text{ is in } P^D\} $$

$$ (\forall p_1, \dots, p_k.P)^\mathcal{I} := \{d \in \Delta^\mathcal{I} \mid \text{every tuple in } p_1^\mathcal{I}(d) \times \dots \times p_k^\mathcal{I}(d) \text{ is in } P^D\}. $$

For example, one can describe individuals having a child that is younger than one of their pets using $\exists \text{child age}, \text{pet age}.$.

# 3 The Expressive Power of $\mathcal{ALCSCC}$

In this section, we first introduce a notion of bisimulation, called Presburger bisimulation, such that $\mathcal{ALCSCC}$ concept descriptions are invariant under such

<footnote>$^4$ In a slight abuse of notation, we view $f^\mathcal{I}(d)$ both as a value and as a singleton set.</footnote>
bisimulations, i.e., bisimilar elements belong to the same ALCSCC concept descriptions. Next, we consider an approximate variant of Presburger bisimulation and show that, while not all ALCSCC concept descriptions are invariant under this notion, the ones that are expressible in first-order logic are. This shows that there are ALCSCC concept descriptions that are not expressible in FOL. Finally, we characterize the fragment of ALCSCC that is first-order definable as the logic ALCQt, for which successor constraints have a restricted form.

**Presburger Bisimulation.** Assume that $N_C$ and $N_R$ are finite. We base our definition of Presburger bisimulations on the notion of safe role types, which are non-empty subsets of $N_R$. Intuitively, such a role type stands for the intersection of its elements intersected with the complements of the non-elements. For example, if $N_R = \{r, s, t\}$, then the safe role type $\{r, s\}$ corresponds to the set term $r \cap s \cap t^c$. More formally, safe role types $\tau$ are interpreted in an interpretation $\mathcal{I}$ as the binary relation

$$ \tau^{\mathcal{I}} := (\bigcap_{r \in \tau} r^{\mathcal{I}} \setminus (\bigcup_{r \in N_R \setminus \tau} r^{\mathcal{I}})) \subseteq \bigcup_{r \in N_R} r^{\mathcal{I}}. $$

The fact that safe role types are non-empty sets of role names ensures the inclusion stated above, i.e., any $\tau^{\mathcal{I}}$ is an $r^{\mathcal{I}}$ successor for at least one role name $r$, which justifies the name safe. Consequently, for all $d \in \Delta^{\mathcal{I}}$, the set $\tau^{\mathcal{I}}(d) := \{e \in \Delta^{\mathcal{I}} | (d, e) \in \tau^{\mathcal{I}}\}$ is a subset of $\text{ars}^{\mathcal{I}}(d)$, and every $e \in \text{ars}^{\mathcal{I}}(d)$ belongs to $\tau^{\mathcal{I}}(d)$ for exactly one safe role type $\tau$. The set $N_R$ must be finite, in order to encode safe role types as well-defined set terms. For ALCSCC$^{\infty}$ it was shown in [7] that each set term $s$ occurring within a succ-restriction can be rewritten as the disjoint union of terms of the form $\tau \cap C$ where $\tau$ is a safe role type and $C$ an ALCSCC$^{\infty}$ concept [7]. The same also holds for ALCSCC. Following [7], we modify the notion of counting bisimulation from [22] by using safe role types in place of role names to obtain Presburger bisimulations (called ALCQt bisimulations in [7]).

**Definition 2.** Let $N_C$ and $N_R$ be finite and $\mathbb{C}$ a class of interpretations. The binary relation $\rho \subseteq \Delta^{\mathcal{I}} \times \Delta^{\mathcal{J}}$ is a Presburger (Pr) bisimulation between the interpretations $\mathcal{I}$ and $\mathcal{J}$ if for all $A \in N_C$ and all safe role types $\tau$ over $N_R$ the following properties are satisfied:

*   **Atomic** $(d, e) \in \rho$ implies $d \in A^{\mathcal{I}}$ iff $e \in A^{\mathcal{J}}$;

*   **Forth** if $(d, e) \in \rho$ and $D \subseteq \tau^{\mathcal{I}}(d)$ is finite, then there is a set $E \subseteq \tau^{\mathcal{J}}(e)$ such that $\rho$ contains a bijection between $D$ and $E$;

*   **Back** if $(d, e) \in \rho$ and $E \subseteq \tau^{\mathcal{J}}(e)$ is finite, then there is a set $D \subseteq \tau^{\mathcal{I}}(d)$ such that $\rho$ contains a bijection between $D$ and $E$.

We call $d \in \Delta^{\mathcal{I}}$ and $e \in \Delta^{\mathcal{J}}$ Pr bisimilar if $(d, e) \in \rho$ for some Pr bisimulation $\rho$ between $\mathcal{I}$ and $\mathcal{J}$. A concept $C$ is $\mathbb{C}$-invariant under Pr bisimulation if $d \in C^{\mathcal{I}}$ iff $e \in C^{\mathcal{J}}$ holds for all Pr bisimilar individuals $d \in \Delta^{\mathcal{I}}$, $e \in \Delta^{\mathcal{J}}$ with $\mathcal{I}, \mathcal{J} \in \mathbb{C}$.

In [7] we proved that ALCSCC$^{\infty}$ concepts are $C_{\text{all}}$-invariant under Pr bisimulation. A very similar proof (by induction on the structure of concept descriptions) can be used to show the corresponding result for ALCSCC, where only finitely branching interpretations are considered.
**Theorem 1.** Every *ALCSCC* concept is *C<sub>fb</sub>*-invariant under *Pr* bisimulation.

*Proof.* Let $\mathcal{I}, \mathcal{J} \in \mathbb{C}_{\text{fb}}$ and $\rho$ a $\text{Pr}$ bisimulation relating $d \in \mathcal{A}^{\mathcal{I}}$ and $e \in \mathcal{A}^{\mathcal{J}}$. We show by induction on the structure of an *ALCSCC* concept $C$ that $d \in C^{\mathcal{I}}$ iff $e \in C^{\mathcal{J}}$ holds. The cases where $C$ is a concept name, a conjunction of concepts or the negation of a concept are similar to the analogous cases in the proof of a corresponding result for *ALC* [13], and are omitted.

Thus, we focus on the case $C = \text{succ(con)}$, where we inductively assume that every subconcept of $C$ is $\mathbb{C}_{\text{fb}}$-invariant under $\text{Pr}$ bisimulation. Recall that *con* is of the form (1). By applying distributivity of set intersection over set union, it is easy to show that any set term occurring in *con* can be written as the disjoint union of set terms of the form $\tau \cap F$ where $\tau$ is a safe role type and $F$ is a Boolean combination of concepts to which the induction assumption applies. The reason we can restrict the attention to safe role types here lies in the semantics of *ALCSCC*, which considers only role successors when evaluating set terms. We provide for every *ALCSCC* concept $F$ and safe role type $\tau$ over $N_{\mathbb{R}}$ an injective mapping from $D := \tau^{\mathcal{I}}(d) \cap F^{\mathcal{I}}$ to $E := \tau^{\mathcal{J}}(e) \cap F^{\mathcal{J}}$ and vice versa. This proves that these sets have the same size, and thus that *con* is evaluated equally w.r.t. $d$ and $e$. Note that, since $\mathcal{I}$ and $\mathcal{J}$ are finitely branching, the sets $D$ and $E$ are both finite. Overall, this implies that $d \in C^{\mathcal{I}}$ iff $e \in C^{\mathcal{J}}$.

The required injections are obtained as follows. Thanks to the *forth* property, we find a set $E' \subseteq \tau^{\mathcal{J}}(e)$ such that $\rho$ contains a bijection between $D$ and $E'$. By our induction hypothesis, the concept $F$ is $\mathbb{C}_{\text{fb}}$-invariant under $\text{Pr}$ bisimulation, so we obtain that $E' \subseteq C^{\mathcal{J}}$. Then, $E' \subseteq E$ holds, and the bijection between $D$ and $E'$ is the sought injective mapping from $D$ to $E$. Using the *back* property, we similarly prove that there is an injective mapping from $E$ to $D$.

Together with the other cases, this concludes our proof, and thus we conclude that every *ALCSCC* concept is *C<sub>fb</sub>*-invariant under *Pr* bisimulation. $\square$

Since finite interpretations are finitely branching, this also implies $\mathbb{C}_{\text{fin}}$-invariance of *ALCSCC* concepts under *Pr* bisimulation.

As usual, such invariance results can be employed to prove that a certain DL $\mathcal{L}$ cannot be expressed in *ALCSCC*. For this, it is sufficient to find an example of an $\mathcal{L}$ concept that is not invariant under $\text{Pr}$ bisimulation. In [11], we apply this approach to show that the abstract expressive power [10] of *ALC*($\mathbb{Q}$) is not contained in that of *ALCSCC* on finitely branching interpretations, and that *ALCSCC<sup>++</sup>* [4] is a strict extension of *ALCSCC* on finite interpretations.

*ALCSCC* goes beyond *FOL* *ALC* and many other DLs are fragments of first-order logic (FOL) [15], in the sense that for every concept description *C* of the given DL there is a *FOL* formula $\phi(x)$ such that $\phi^{\mathcal{I}} = C^{\mathcal{I}}$ for all interpretations $\mathcal{I}$, where $\phi^{\mathcal{I}} := \{d \in \mathcal{D}^{\mathcal{I}} | \mathcal{I} \models \phi(d)\}$. This notion of definability of a concept description by an *FOL* formula in one free variable can be relativized to a class of models $\mathbb{C}$ in an obvious way. *C*-invariance of an *FOL* formula in one free variable under a given notion of bisimulation is also defined in an obvious way.

In [7], we have shown that there are *ALCSCC*<sup>∞</sup> concepts that are not *FOL*-definable in this sense w.r.t. $\mathbb{C}_{\text{all}}$. However, since the semantics of *ALCSCC* is
defined w.r.t. a restricted class of interpretations, this result does not directly transfer to *ALCSCC*. Our tool for showing non-FOL-definability for *ALCSCC* (and incidentally also for *ALCSCC*∞ w.r.t. other classes of interpretations) is a bounded version of *Pr* bisimulation where one makes only a bounded number *ℓ* of steps into the interpretation and bounds the cardinalities of the sets considered in the back and forth conditions by a number *q*. This notion of bisimulation is obtained by adapting the bisimulation-based characterization of modal logic with graded modalities w.r.t. finite models in [25] to our more expressive logic.

**Definition 3.** Let $N_C$ and $N_R$ be finite and $q, \ell \in \mathbb{N}$. The relation $\rho \subseteq \Delta^I \times \Delta^J$ is a $\mathbf{Pr}$ $(q,0)$-bisimulation between the interpretations $\mathcal{I}$ and $\mathcal{J}$ if it satisfies the (atomic) condition of Definition 2, and it is a $\mathbf{Pr}$ $(q,\ell+1)$-bisimulation if it is a $\mathbf{Pr}$ $(q,\ell)$-bisimulation that satisfies the following for all safe role types $\tau$:

(q,ℓ)-forth if $(d,e) \in \rho$ and $D \subseteq \tau^I(d)$ with $|D| \le q$, then there are $E \subseteq \tau^J(e)$ and a $\mathbf{Pr}$ $(q,\ell)$-bisimulation $\rho'$ that contains a bijection between $D$ and $E$;

(q,ℓ)-back if $(d,e) \in \rho$ and $E \subseteq \tau^J(e)$ with $|E| \le q$, then there are $D \subseteq \tau^I(d)$ and a $\mathbf{Pr}$ $(q,\ell)$-bisimulation $\rho'$ that contains a bijection between $D$ and $E$.

The notions of $\mathbf{Pr}$ $(q,\ell)$-bisimilarity and $\mathbb{C}$-invariance w.r.t. $\mathbf{Pr}$ $(q,\ell)$-bisimulation are defined similarly to how it was done in Definition 2.

Theorem 1 states that all *ALCSCC* concepts are invariant under *Pr* bisimula-
tion. For *Pr* $(q,\ell)$-bisimulation, this need not hold, as stated in the next theorem.

**Theorem 2.** There is an *ALCSCC* concept *C* such that, for all values of *q* and *ℓ*, the concept *C* is not *C*<sub>*fb*</sub>-invariant under *Pr* (*q*,*ℓ*)-bisimulation.

*Proof.* Consider the *ALCSCC* concept $C := \mathbf{succ}(|r \cap A| = |r \cap \neg A|)$, which has been used in [7] to show that *ALCSCC*<sup>∞</sup> is not a fragment of FOL. For $n, m \in \mathbb{N}$, let $\mathcal{I}_{m,n}$ be the finitely branching interpretation containing individuals $d$ and $d_i$ for $i = 1, \dots, m+n$, where $r$ is interpreted as the set of tuples $(d, d_i)$ for $i = 1, \dots, m+n$, every $d_i$ with $i = 1, \dots, m$ is in $A$ and every other individual is not in $A$. Given $q \in \mathbb{N}$ we consider $\mathcal{I}_{q,q}$ and $\mathcal{I}_{q,q+1}$, and notice that $d \in \mathcal{I}_{q,q}$ and $d \in \mathcal{I}_{q,q+1}$ are $\mathbf{Pr}$ $(q,\ell)$-bisimilar: the relation mapping $d \in \mathcal{I}_{q,q}$ to $d \in \mathcal{I}_{q,q+1}$ and $d_i \in \mathcal{I}_{q,q}$ to $d_i \in \mathcal{I}_{q,q+1}$ is a $\mathbf{Pr}$ $(q,\ell)$-bisimulation for all $\ell \in \mathbb{N}$. However, $d \in C^{\mathcal{I}_{q,q}}$ holds, whereas $d \notin C^{\mathcal{I}_{q,q+1}}$. $\square$

Our goal is now to show that this cannot happen for *ALCSCC* concepts that
are FOL-definable w.r.t. *C<sub>fb</sub>* or *C<sub>fin</sub>* (or more generally a class *C* of interpretations
satisfying certain closure properties). The proof of this result uses certain locality
properties of FOL formulae that are invariant under *Pr* bisimulation.

**Definition 4.** Let $\mathcal{I}$ be an interpretation. The distance of $d$ and $d'$ in $\mathcal{I}$ is the smallest value $\ell \in \mathbb{N}$ for which there is a sequence of elements $d_1, \dots, d_{\ell+1} \in \Delta^I$ where $d_1 = d$, $d_{\ell+1} = d'$ and $d_i$ is a role successor or predecessor of $d_{i+1}$ for $i = 1, \dots, \ell$, or $\infty$ if such a number does not exist. The $\ell$-neighborhood $\mathcal{N}_{\ell}^{\mathcal{I}}[d]$
of d is derived from $\mathcal{I}$ by taking the substructure consisting of all individuals with distance at most $\ell$ from d.

The class $\mathbb{C}$ of interpretations is closed under neighborhoods if $N_{\ell}^{\mathcal{I}}[d] \in \mathbb{C}$ for all $\mathcal{I} \in \mathbb{C}$, $d \in \Delta^{\mathcal{I}}$ and $\ell \in \mathbb{N}$. The FOL formula $\phi(x)$ is $\ell$-local w.r.t. $\mathbb{C}$ if for all $\mathcal{I} \in \mathbb{C}$ and all $d \in \Delta^{\mathcal{I}}$ we have that $\mathcal{I} \models \phi(d)$ iff $N_{\ell}^{\mathcal{I}}[d] \models \phi(d)$.

Interestingly, there is a close relationship between $\ell$-locality of FOL formulae and invariance under finite disjoint union.

**Definition 5 (Disjoint union).** Given a finite index set $\mathbb{I}$ and a family of interpretations $(\mathcal{I}_{\nu})_{\nu \in \mathbb{I}} \subseteq \mathbb{C}$, their finite disjoint union $\mathcal{I}$ is defined by:

$$ \Delta^{\mathcal{I}} := \{(d, \nu) \mid \nu \in \mathbb{I} \text{ and } d \in \Delta^{\mathcal{I}_{\nu}}\}, $$

$$ A^{\mathcal{I}} := \{(d, \nu) \mid \nu \in \mathbb{I} \text{ and } d \in A^{\mathcal{I}_{\nu}}\} \text{ for all } A \in \mathbb{N}_{\mathbb{C}}, $$

$$ r^{\mathcal{I}} := \{((d, \nu), (e, \nu)) \mid \nu \in \mathbb{I} \text{ and } (d, e) \in r^{\mathcal{I}_{\nu}}\} \text{ for all } r \in \mathbb{N}_{\mathbb{R}}. $$

The FOL formula $\phi(x)$ is $\mathbb{C}$-invariant under finite disjoint unions if, for any finite disjoint union constructed as above, $\mathcal{I}_{\nu} \models \phi(d)$ iff $\mathcal{I} \models \phi((d, \nu))$ holds for every $\nu \in \mathbb{I}$ and $d \in \Delta^{\mathcal{I}_{\nu}}$. We say that $\mathbb{C}$ is closed under finite disjoint unions if $\mathcal{I}_{\nu} \in \mathbb{C}$ for all $\nu \in \mathbb{I}$ implies that the disjoint union of $(\mathcal{I}_{\nu})_{\nu \in \mathbb{I}}$ also belongs to $\mathbb{C}$ whenever the index set $\mathbb{I}$ is finite.

By proving that $\rho := \{(d, (d, \nu)) \mid d \in \Delta^{\mathcal{I}_{\nu}}, \nu \in \mathbb{I}\}$ is a $\text{Pr}$ bisimulation, we obtain the following property for formulae that are $\mathbb{C}$-invariant under $\text{Pr}$ bisimulation.

**Proposition 1.** If the FOL formula $\phi(x)$ is $\mathbb{C}$-invariant under $\text{Pr}$ bisimulation, then it is $\mathbb{C}$-invariant under finite disjoint unions.

By Theorem 1, this implies that FOL formulae that are equivalent to $\mathcal{ALCSCC}$ concepts are $\mathbb{C}_{\text{fb}}$- and $\mathbb{C}_{\text{fin}}$-invariant under disjoint union. Before we can state the crucial lemma from [24], we must introduce one more notation. We call the class $\mathbb{C}$ of interpretations localizable if it is closed under both neighborhoods and finite disjoint unions.<fnref n="5" /> Note that our classes $\mathbb{C}_{\text{all}}$, $\mathbb{C}_{\text{fb}}$ and $\mathbb{C}_{\text{fin}}$ are localizable.

**Lemma 1 ([24]).** If $\mathbb{C}$ is localizable, then any FOL formula $\phi(x)$ of quantifier depth $q$ that is $\mathbb{C}$-invariant under finite disjoint unions is $(2^q - 1)$-local w.r.t. $\mathbb{C}$.

Combining this lemma with Proposition 1, we can now link $\ell$-locality with invariance under $\text{Pr}$ bisimulation.

**Corollary 1.** If $\mathbb{C}$ is localizable, then any FOL formula $\phi(x)$ of quantifier depth $q$ that is $\mathbb{C}$-invariant under $\text{Pr}$ bisimulation is $\ell$-local w.r.t. $\mathbb{C}$ for $\ell := 2^q - 1$.

Our next goal is now to show that, for FOL formulae, invariance under $\text{Pr}$ bisimulation is equivalent to invariance under $\text{Pr}$ $(q, \ell)$-bisimulation for some $q, \ell \in \mathbb{N}$. Our first step in this direction is the following result for trees, whose proof can be found in [11].

<footnote n="5">⁵ These conditions on $\mathbb{C}$ are not stated explicitly in [24], but are implicitly assumed.</footnote>
**Theorem 3.** If $\mathcal{I}$, $\mathcal{J}$ are trees of depth at most $\ell$ with roots $d$, $e$ that are $\mathrm{Pr}(q, \ell)$-bisimilar, then these roots satisfy the same FOL formulae $\phi(x)$ of quantifier depth at most $q$.

While not all interpretations in a class $\mathbb{C}$ need to be tree-shaped, we show that, for every interpretation in $\mathbb{C}_{\mathrm{all}}$, $\mathbb{C}_{\mathrm{fb}}$ or $\mathbb{C}_{\mathrm{fin}}$, it is possible to find a $\mathrm{Pr}$ bisimilar interpretation in this class where the $\ell$-neighborhood of a specific individual $d$ is a tree with root $d$. Normally, this is achieved by unravelling [13], but this may yield an infinite interpretation, and is thus not suitable for our setting, where we are also interested in the class $\mathbb{C}_{\mathrm{fin}}$. Instead, we introduce *partial unravelling* of $\mathcal{I}$, which preserves finiteness and (like unraveling) finite branching. Intuitively, the $\ell$-unravelling of an interpretation $\mathcal{I}$ at an element $d \in \Delta^{\mathcal{I}}$ applies unraveling up to length $\ell$, and then adds a copy of $\mathcal{I}$ at the end. The exact definition of this operation, which is an adaptation of the unravelling operation described in [13], can be found in [11]. Here, we only state two important properties of it.

**Proposition 2.** Let $\mathcal{I}_{\ell}^{d}$ be the $\ell$-unravelling of the interpretation $\mathcal{I}$ at $d \in \Delta^{\mathcal{I}}$, $\langle d \rangle$ the element corresponding to $d$ in $\mathcal{I}_{\ell}^{d}$. Then,

1. The elements $d \in \Delta^{\mathcal{I}}$ and $\langle d \rangle \in \Delta_{\ell}^{\mathcal{I}^{d}}$ are $\mathrm{Pr}$ bisimilar.

2. The $\ell$-neighborhood $\mathcal{N}_{\ell}^{\mathcal{I}^{d}}[\langle\langle d \rangle\rangle]$ of $\langle d \rangle$ in $\mathcal{I}_{\ell}^{d}$ is a tree of depth at most $\ell$ with root $\langle d \rangle$.

The class $\mathbb{C}$ of interpretations is closed under *partial unravelling* if $\mathcal{I} \in \mathbb{C}$ implies $\mathcal{I}_{\ell}^{d} \in \mathbb{C}$ for all $\ell \in \mathbb{N}$. The following result links invariance under $\mathrm{Pr}$ bisimulation with invariance under $\mathrm{Pr}(q, \ell)$-bisimulation for FOL formulae.

**Theorem 4.** Let $\mathbb{C}$ be localizable and closed under *partial unravelling*. For all FOL formulae $\phi(x)$, the following are equivalent:

1. $\phi(x)$ is $\mathbb{C}$-invariant under $\mathrm{Pr}$ bisimulation.

2. $\phi(x)$ is $\mathbb{C}$-invariant under $\mathrm{Pr}(q, \ell)$-bisimulation for some $q, \ell \in \mathbb{N}$.

*Proof.* The implication “2. ⇒ 1.” is an immediate consequence of the fact that every $\mathrm{Pr}$ bisimulation is also a $\mathrm{Pr}(q, \ell)$-bisimulation for all $q, \ell \in \mathbb{N}$.

To prove the other direction, we assume 1. and that $\phi(x)$ has quantifier depth $q$. By assume 1 we deduce that $\phi(x)$ is $\ell$-local w.r.t. $\mathbb{C}$ for $\ell := 2^q - 1$. Given $\mathcal{I}, \mathcal{J} \in \mathbb{C}$ and $d \in \Delta^{\mathcal{I}}, e \in \Delta^{\mathcal{J}}$, we know that the $\ell$-unravellings $\mathcal{I}_{\ell}^{d}$ and $\mathcal{J}_{\ell}^{e}$ and the $\ell$-neighborhoods $\mathcal{N}_{d} := \mathcal{N}_{\ell}^{\mathcal{I}^{d}}[\langle\langle d \rangle\rangle]$ and $\mathcal{N}_{e} := \mathcal{N}_{\ell}^{\mathcal{J}^{e}}[\langle\langle e \rangle\rangle]$ also belong to $\mathbb{C}$. Since $\phi(x)$ is $\mathbb{C}$-invariant under $\mathrm{Pr}$ bisimulation and $\ell$-local w.r.t. $\mathbb{C}$ we obtain

$$ \begin{aligned} \mathcal{I} &\models \phi(d) \text{ iff } \mathcal{I}_{\ell}^{d} \models \phi(\langle d \rangle) \text{ iff } \mathcal{N}_{d} \models \phi(\langle d \rangle) \text{ and} \\ \mathcal{J} &\models \phi(e) \text{ iff } \mathcal{J}_{\ell}^{e} \models \phi(\langle e \rangle) \text{ iff } \mathcal{N}_{e} \models \phi(\langle e \rangle). \end{aligned} \quad \text{(by Proposition 2)} $$

If $\rho$ is a $\mathrm{Pr}(q, \ell)$-bisimulation with $(d, e) \in \rho$, then combining this relation with the $\mathrm{Pr}$ bisimulations linking $d$ and $\langle d \rangle$ and $e$ and $\langle e \rangle$ shows that there is a $\mathrm{Pr}(q, \ell)$-bisimulation $\rho'$ between $\mathcal{I}_{\ell}^{d}$ and $\mathcal{I}_{\ell}^{e}$ with $(\langle d \rangle, \langle e \rangle) \in \rho'$. Since such a bisimulation
looks only $\ell$ steps into the interpretation, the restriction of $\rho'$ to the respective $\ell$-neighborhoods $N_d$ and $N_e$ is also a Pr $(q, \ell)$-bisimulation. Proposition 2 says that these neighborhoods are trees of depth at most $\ell$, and thus we can apply Theorem 3 to obtain $N_d \models \phi(\langle d \rangle)$ iff $N_e \models \phi(\langle e \rangle)$. $\square$

<figure><img src="image_15.png" /></figure>

Together with Theorem 2, this yields the desired non-definability results since the classes $C_{\text{all}}$, $C_{\text{fb}}$, and $C_{\text{fin}}$ are localizable and closed under partial unravelling.

**Corollary 2.** Let $\mathbb{C}$ be localizable and closed under partial unravelling. Then there are ALCSCC concepts that are not FOL-definable w.r.t. $\mathbb{C}$.

**The first-order fragment of ALCSCC.** In [7], we have established that the FOL-definable subset of $ALCSCC^{\infty}$ corresponds to the DL $ALCQt$. This DL can be seen both as the extension of $ALCQ$ where safe role types instead of just role names can be used in qualified number restrictions, and as the restriction of $ALCSCC$ where only successor restrictions of the form $succ(|\tau \cap C| \ge q)$ are available, where $\tau$ is a safe role type, $q \in \mathbb{N}$, and $C$ is an $ALCQt$ concept. To make the relationship to qualified number restrictions clear, we write such successor restrictions as $(\ge q \tau \cdot C)$, and call them qualified number restrictions. Saying that this result was proved in [7] for $ALCSCC^{\infty}$ means that it was shown w.r.t. the class $C_{\text{all}}$. In the following we prove that it also holds for the classes $C_{\text{fb}}$ and $C_{\text{fin}}$.

It is easy to see that every $ALCQt$ concept can be translated into an equiv-
alent FOL formula with one free variable, and thus $ALCQt$ is a FOL-definable
fragment of $ALCSCC$. We will show that all FOL-definable concepts of $ALCSCC$
are equivalent to one in $ALCQt$. We define the depth of an $ALCQt$ concept to be
the maximal nesting of qualified number restrictions and the breadth to be the
maximal number occurring in a qualified number restriction. With $ALCQt_{q,\ell}$ we
denote the set of $ALCQt$ concepts of depth at most $\ell$ and breadth at most $q$.
The following results for $ALCQt_{q,\ell}$ are established in [11].

**Proposition 3.** Let $\mathbb{C}$ be a class of interpretations, $q, \ell \in \mathbb{N}$, and assume that $N_{\mathbb{C}}$ and $N_{\mathbb{R}}$ are finite. Then the following holds:

1. Every $ALCQt_{q,\ell}$ concept is $\mathbb{C}$-invariant under $\text{Pr}(q,\ell)$-bisimulation.

2. Up to $\mathbb{C}$-equivalence, there are only finitely many $ALCQt_{q,\ell}$ concepts.

3. For every $\mathcal{I} \in \mathbb{C}$ and $d \in \Delta^{\mathcal{I}}$ there is an $ALCQt_{q,\ell}$ concept $\text{Bisim}_{\ell}^{q}[d]$ such that $d \in \text{Bisim}_{\ell}^{q}[d]^{\mathcal{I}}$ and $e \in \text{Bisim}_{\ell}^{q}[d]^{\mathcal{J}}$ for an interpretation $\mathcal{J} \in \mathbb{C}$ and $d \in \Delta^{\mathcal{J}}$ implies that $d$ and $e$ are $(q,\ell)$-bisimilar.

Combining these results with Theorems 1 and 4, we obtain the following
characterization of the FOL fragment on $ALCSCC$.

**Theorem 5.** Let $\mathbb{C}$ be localizable and closed under partial unravelling and $N_{\mathbb{C}}$, $N_{\mathbb{R}}$ be finite. For all FOL formulae $\phi(x)$, the following are equivalent:

1. $\phi(x)$ is $\mathbb{C}$-equivalent to some ALCSCC concept.

2. $\phi(x)$ is $\mathbb{C}$-invariant under $\text{Pr}$ bisimulation.

3. $\phi(x)$ is $\mathbb{C}$-invariant under $\text{Pr}(q,\ell)$-bisimulation for some $q, \ell \in \mathbb{N}$.
4. $\phi(x)$ is $\mathbb{C}$-equivalent to some $\mathcal{ALCQt}$ concept.

*Proof.* That 1. implies 2. follows from Theorem 1 and the equivalence between 2. and 3. is stated in Theorem 4. In addition, 4. trivially implies 1.

Thus, it is sufficient to show that 3. implies 4. To this purpose, we define $C_{\phi} := \bigcup\{\text{Bisim}_{\ell}^{q}[d] \mid \mathcal{I} \in \mathbb{C}, d \in \Delta^{\mathcal{I}} \text{ and } \mathcal{I} \models \phi(d)\}$. By 2. of Proposition 3, this disjunction is finite (up to equivalence), and thus $C_{\phi}$ is a well-formed $\mathcal{ALCQt}_{q,\ell}$ concept. First, assume that $\mathcal{I} \models \phi(d)$ with $\mathcal{I} \in \mathbb{C}$ and $d \in \Delta^{\mathcal{I}}$. Then, $d \in C_{\phi}^{\mathcal{I}}$ trivially follows from the fact that $\text{Bisim}_{\ell}^{q}[d]$ occurs as a disjunct in $C_{\phi}$.

Conversely, if $d \in C_{\phi}^{\mathcal{I}}$, then $d \in (\text{Bisim}_{\ell}^{q}[e])^{\mathcal{I}}$ for some $\mathcal{J} \in \mathbb{C}$ and $e \in \Delta^{\mathcal{J}}$ such that $\mathcal{J} \models \phi(e)$. By 3. of Proposition 3, this implies that $d$ and $e$ are $\text{Pr}(q,\ell)$-bisimilar. Hence, 3. of the present proposition implies that $\mathcal{I} \models \phi(d)$. Thus, we have shown that $\phi(x)$ and $C_{\phi}$ are $\mathbb{C}$-equivalent. $\square$

Recall that the classes $C_{\text{all}}$, $C_{\text{fb}}$ or $C_{\text{fin}}$ satisfy the assumptions of Theorem 5.

# 4 The Expressive Power of DLs with Concrete Domains

In [9,10] we have investigated the *abstract expressive power* of DLs with concrete domains, which only considers the abstract part of interpretations, i.e., ignores the values assigned to features. This allowed us to compare classical logics like *ALC* and *FOL* with DLs with concrete domains. Here, we want to compare extensions of *ALC* with different concrete domains using an appropriate notion of bisimulation, called *D* bisimulation if *D* is the concrete domain under consideration, and characterize *ALC(D)* as the fragment of *FOL(D)* that is invariant under *D* bisimulation. The employed notion of bisimulation is the one for *ALC* (see, e.g., [13]) extended with an additional clause that deals with feature values. As in the previous section, we show our results not only for the class of all interpretations, but also for the restrictions to finitely branching and finite ones.

**Definition 6.** Let $\mathcal{D}$ be a concrete domain and $\mathcal{I}, \mathcal{J}$ interpretations of $N_{\mathbb{C}}, N_{\mathbb{R}}$ and $N_{\mathbb{F}}$ that assign elements of $\mathcal{D}$ to features from $N_{\mathbb{F}}$. The relation $\rho \subseteq \Delta^{\mathcal{I}} \times \Delta^{\mathcal{J}}$ is a $\mathcal{D}$ bisimulation between $\mathcal{I}$ and $\mathcal{J}$ if for all $A \in N_{\mathbb{C}}, \text{ all } r \in N_{\mathbb{R}}, \text{ all } k$-ary relations $P$ of $\mathcal{D}$, and all feature paths $p_1, \dots, p_k$ over $N_{\mathbb{R}}$ and $N_{\mathbb{F}}$:

**atomic** if $(d,e) \in \rho$ then $d \in A^{\mathcal{I}}$ iff $e \in A^{\mathcal{J}}$;

**forth** if $(d,e) \in \rho$ and $d' \in r^{\mathcal{I}}(d)$, then there is $e' \in r^{\mathcal{J}}(e)$ such that $(d', e') \in \rho$;

**back** if $(d,e) \in \rho$ and $e' \in r^{\mathcal{J}}(e)$, then there is $d' \in r^{\mathcal{I}}(d)$ such that $(d', e') \in \rho$.

**features** if $(d,e) \in \rho$, then there is $(v_1, \dots, v_k) \in P^D$ with $v_1 \in p_1^{\mathcal{I}}(d), \dots, v_k \in p_k^{\mathcal{I}}(d)$ iff there is $(w_1, \dots, w_k) \in P^D$ with $w_1 \in p_1^{\mathcal{J}}(e), \dots, w_k \in p_k^{\mathcal{J}}(e)$.

*Bisimilarity between individuals and $\mathbb{C}$-invariance w.r.t. $\mathcal{D}$ bisimulation are defined similarly to how it was done in Definition 2 w.r.t. Pr bisimulation.*

A result analogous to Theorem 1 holds for $\mathcal{ALC}(\mathcal{D})$ concepts if the concrete domain $\mathcal{D}$ is weakly closed under negation.
**Theorem 6.** If $\mathcal{D}$ is WCUN and $\mathbb{C}$ is a class of interpretations of $\mathbb{N}_C$, $\mathbb{N}_R$ and $\mathbb{N}_F$ that assign elements of $\mathcal{D}$ to features from $\mathbb{N}_F$, then every $\mathcal{ALC}(\mathcal{D})$ concept is $\mathbb{C}$-invariant under $\mathcal{D}$ bisimulation.

*Proof.* The proof by structural induction on the concept $C$ proceeds like the one for $\mathcal{ALC}$ in [13], except for the cases where $C$ is a CD-restriction. We only consider these cases explicitly here. Thus, let $\rho$ be a $\mathcal{D}$ bisimulation between $\mathcal{I}$ and $\mathcal{J}$ with $(d, e) \in \rho$. We show that $d$ and $e$ satisfy the same CD-restrictions.

If $C := \exists p_1, \dots, p_k.P$ then $d \in C^I$ implies the existence of $v_1 \in p_1^I(d), \dots, v_k \in p_k^I(d)$ such that $(v_1, \dots, v_k) \in P^D$. Since $\rho$ satisfies features, there must be $w_1 \in p_1^J(e), \dots, w_k \in p_k^J(e)$ such that $(w_1, \dots, w_k) \in P^D$, hence $e \in C^J$. Similarly, we can show that $e \in C^J$ implies $d \in C^I$.

If $C := \forall p_1, \dots, p_k.P$, then $d \in C^I$ implies that $(v_1, \dots, v_k) \in P^D$ for all values $v_1 \in p_1^I(d), \dots, v_k \in p_k^I(d)$. Since $\mathcal{D}$ is WCUN, this is the case iff there are relations $P_1, \dots, P_{n_P}$ of $\mathcal{D}$ such that $(v_1, \dots, v_k) \notin P_i^D$ for $i = 1, \dots, n_P$. Using the features condition of $\rho$, we deduce that $(w_1, \dots, w_k) \notin P_i^D$ for all $w_1 \in p_1^J(e), \dots, w_k \in p_k^J(e)$ and $i = 1, \dots, n_P$. By WCUN it follows that $(w_1, \dots, w_k) \in P^D$, and we conclude that $e \in C^J$. The proof of the other direction is symmetric. $\square$

**A Non-expressivity Result.** We can use the notion of $\mathcal{D}$ bisimulation to show that $\mathcal{ALC}(\mathcal{D})$ cannot express certain concepts of the DL $\mathcal{ALC}(\mathcal{D}')$, where $\mathcal{D}'$ has the same domain set as $\mathcal{D}$, but different relations. Coming back to the example in the introduction, we compare the expressive power of $\mathfrak{Q}_{+1}$ and $\mathfrak{Q}_{+2}$, both having domain set $\mathbb{Q}$, where the former has a binary relation $+1$ relating $q \in \mathbb{Q}$ and $q+1$ (and the complementary relation $\neq_{+1}$) and the latter has a binary relation $+2$ relating $q$ and $q+2$ (and the complementary relation $\neq_{+2}$).

These two DLs have the same abstract *expressive power*. In fact, we can interchange CD-restrictions using relations $+1$ and $\neq_{+1}$ with restrictions of the same kind (existential or universal) using relations $+2$ and $\neq_{+2}$. Abstract models of a concept in one of these DLs are then the same as of the corresponding concept in the other DL: in one direction we just double the feature values, and in the other we halve them. Nevertheless, we can show that their concrete *expressive power*, which takes the feature values into account, is incomparable.

**Proposition 4.** Let $\mathbb{C}$ be $\mathbb{C}_{\text{all}}$, $\mathbb{C}_{\text{rb}}$, or $\mathbb{C}_{\text{fin}}$. There are $\mathcal{ALC}(\mathfrak{Q}_{+1})$ concepts that are not $\mathbb{C}$-equivalent to any $\mathcal{ALC}(\mathfrak{Q}_{+2})$ concept (and vice versa).

*Proof.* First, consider the $\mathcal{ALC}(\mathfrak{Q}_{+1})$ concept $C := \exists rf, rf.+1$ and assume by contradiction that it is $\mathbb{C}_{\text{all}}$-equivalent to some $\mathcal{ALC}(\mathfrak{Q}_{+2})$ concept $D$. Let us consider the interpretations $\mathcal{I}$ and $\mathcal{J}$ depicted in Fig. 1. Then, $a \in C^I$ and by equivalence $a \in D^I$, while $a_1 \notin C^J$ and so $a_1 \notin D^J$ by equivalence. This leads to a contradiction, since the relation $\rho$ between $\mathcal{I}$ and $\mathcal{J}$ is a $\mathfrak{Q}_{+2}$ bisimulation relating $a$ and $a_1$, and by Theorem 6 this means that $a \in D^I$ iff $a_1 \in D^J$. Therefore, we conclude that $C$ and $D$ cannot be equivalent w.r.t. any class of interpretations that contains the two interpretations of Fig. 1. Vice versa, we can show with a similar argument that $\exists rf, rf.+2$ cannot be expressed in $\mathcal{ALC}(\mathfrak{Q}_{+1})$, but this requires slightly different interpretations. $\square$
<figure><img src="image_16.png" /><figcaption>Fig. 1. A $\Omega_{+2}$ bisimulation $\rho$ between $\mathcal{I}$ (left) and $\mathcal{J}$ (right).</figcaption></figure>

**FOL with concrete domains and ALC($\mathcal{D}$).** Since we are interested in characterizing the concrete expressive power of ALC($\mathcal{D}$), which takes the feature values into account, we cannot compare ALC($\mathcal{D}$) with FOL, where no such values are available. Instead, we consider the extension FOL($\mathcal{D}$) of FOL with the concrete domain $\mathcal{D}$ as introduced in [9,10]. The logic FOL($\mathcal{D}$) is obtained from FOL by adding *definedness predicates* Def($f$)($t$) with $f \in \mathbf{N}_F$ and $t$ a first-order term, and concrete domain predicates $P(f_1, \dots, f_k)(t_1, \dots, t_k)$ where $P$ is a $k$-ary relation of $\mathcal{D}$, each $t_i$ is a first-order term and $f_i \in \mathbf{N}_F$ for $i = 1, \dots, k$.

The semantics of FOL($\mathcal{D}$) formulae is defined in terms of first-order interpretations $\mathcal{I} = (\Delta^{\mathcal{I}}, \mathcal{I})$ that additionally assign partial functions $f^{\mathcal{I}}: \Delta^{\mathcal{I}} \to \mathcal{D}$ to $f \in \mathbf{N}_F$. The semantics of terms, Boolean connectives and first-order quantifiers is defined as usual. Denoting the interpretation of a first-order term $t$ w.r.t $\mathcal{I}$ and a variable assignment $w$ as $t^{\mathcal{I},w}$, the new predicates are interpreted as follows:

$$ - \mathcal{I} \models \text{Def}(f)(t^{\mathcal{I},w}) \text{ if } f^{\mathcal{I}}(t^{\mathcal{I},w}) \text{ is defined, and} $$

$$ - \mathcal{I} \models P(f_1, \dots, f_k)(t_1^{\mathcal{I},w}, \dots, t_k^{\mathcal{I},w}) \text{ if } (f_1^{\mathcal{I}}(t_1^{\mathcal{I},w}), \dots, f_k^{\mathcal{I}}(t_k^{\mathcal{I},w})) \in \mathcal{P}^{\mathcal{D}}. $$

Note that if $(f_1^{\mathcal{I}}(t_1^{\mathcal{I},w}), \dots, f_k^{\mathcal{I}}(t_k^{\mathcal{I},w})) \in \mathcal{P}^{\mathcal{D}}$ then each $f_i^{\mathcal{I}}(t_i^{\mathcal{I},w})$ must be defined.

It is easy to see (and explicitly shown in [9,10]) that ALC($\mathcal{D}$) is a fragment of FOL($\mathcal{D}$). Our goal is to prove that it is the fragment of FOL($\mathcal{D}$) that is invariant under $\mathcal{D}$ bisimulation, not just for the class of all interpretations, but also for finite and finitely branching interpretations. For this, we use an approach that is very similar to the one employed in Sect. 3. Recall that Lemma 1 turned out to be an important model-theoretic tool in that approach since it provided us with locality results for FOL formulae expressing ALCSCC concepts. The corresponding result also holds for FOL($\mathcal{D}$). Note that the notions of *finite disjoint union* and the corresponding $\mathbb{C}$-invariance w.r.t. classes $\mathbb{C}$ of interpretations of $\mathbf{N}_C$, $\mathbf{N}_R$ and $\mathbf{N}_F$ are obtained by extending Definition 5 to account for feature names in the obvious way. For interpretations of $\mathbf{N}_C$, $\mathbf{N}_R$ and $\mathbf{N}_F$ we define $\ell$-neighborhoods by using the same notion of distance employed in Definition 4. This means that the distance of two individuals is not determined by concrete domain predicates, but only by role names. The notions of $\ell$-locality of a FOL($\mathcal{D}$) formula and of $\mathbb{C}$-invariance w.r.t. classes $\mathbb{C}$ of interpretations of $\mathbf{N}_C$, $\mathbf{N}_R$ and $\mathbf{N}_F$ are obtained by extending Definition 4 using this notion of neighborhood. In particular, the extension of the classes $\mathbb{C}_{\text{all}}$, $\mathbb{C}_{\text{fb}}$, and $\mathbb{C}_{\text{fin}}$ to interpretations taking feature names into account are defined in the obvious way, and these classes are localizable.
**Lemma 2.** If $\mathbb{C}$ is localizable, then a FOL($\mathbb{D}$) formula $\phi(x)$ of quantifier depth $q$ that is $\mathbb{C}$-invariant under disjoint unions is $\ell$-local w.r.t. $\mathbb{C}$ for $\ell := 2^q - 1$.

This result can be proved similarly to Lemma 1, by employing the translation of FOL($\mathbb{D}$) formulae and FOL($\mathbb{D}$) interpretations into FOL formulae and FOL interpretations introduced in [9, 10] (see [11] for details).

In the following, we assume that the concrete domain $\mathbb{D}$ is WCUN and has finitely many relations; both conditions are always satisfied by $\omega$-admissible concrete domains [14,21]. Following the approach employed in the previous section, we introduce a bounded version of $\mathbb{D}$ bisimulation, where now only the depth is bounded since there are no cardinality constraints.

**Definition 7.** Let $\mathcal{I}$, $\mathcal{J}$ be interpretations of $N_{\mathbb{C}}$, $N_{\mathbb{R}}$ and $N_{\mathbb{F}}$ and $\ell \in \mathbb{N}$. The relation $\rho \subseteq \Delta^{\mathcal{I}} \times \Delta^{\mathcal{J}}$ is a $\mathbb{D}$-0-bisimulation if $\rho$ satisfies the *atomic condition* of Definition 6 and for all $k$-ary relations $P$ of $\mathbb{D}$ and $f_1, \dots, f_k \in N_{\mathbb{F}}$:

**values** if $(d,e) \in \rho$ then $(f_1^{\mathcal{I}}(d), \dots, f_k^{\mathcal{I}}(d)) \in P^D$ iff $(f_1^{\mathcal{J}}(e), \dots, f_k^{\mathcal{J}}(e)) \in P^D$.

The relation $\rho$ is a $\mathbb{D}$ ($\ell + 1$)-bisimulation if it is a $\mathbb{D}\ell$-bisimulation that additionally satisfies the *features* conditions of Definition 6, and for all $r \in N_{\mathbb{R}}$ the following are satisfied:

* $\ell$-forth if $(d,e) \in \rho$ and $d'$ is an $r$-successor of $d$, then there exist an $r$-successor $e'$ of $e$ and a $\mathbb{D}\ell$-bisimulation $\rho'$ such that $(d', e') \in \rho'$;

* $\ell$-back if $(d,e) \in \rho$ and $e'$ is an $r$-successor of $e$, then there exist an $r$-successor $d'$ of $d$ and a $\mathbb{D}\ell$-bisimulation $\rho'$ such that $(d', e') \in \rho'$.

The notions of bisimilarity and $\mathbb{C}$-invariance w.r.t. $\mathbb{D}\ell$-bisimulation are defined similarly to how it was done in Definition 2.

In [11] we show that, under the assumption that the concrete domain $\mathbb{D}$ is WCUN and has finitely many relations, results analogous to Proposition 1, Corollary 1, Theorem 3, Proposition 2, Theorem 4, and Proposition 3 also hold for FOL($\mathbb{D}$) and $\mathcal{ALC}(\mathbb{D})$, where $\mathcal{ALC}(\mathbb{D})$ plays both the role of $\mathcal{ALCSCC}$ and of $\mathcal{ALCQt}$. Similarly to the proof of Theorem 4, these results can be combined to show the following characterization of $\mathcal{ALC}(\mathbb{D})$ as the fragment of FOL($\mathbb{D}$) that is invariant under $\mathbb{D}$ bisimulation.

**Theorem 7.** Let $\mathbb{C}$ be localizable and closed under partial unravelling, $\mathbb{D}$ be WCUN and have finitely many relations, and $N_{\mathbb{C}}$, $N_{\mathbb{R}}$, $N_{\mathbb{F}}$ be finite. Then the following are equivalent for all FOL($\mathbb{D}$) formulae $\phi(x)$:

1. $\phi(x)$ is $\mathbb{C}$-invariant under $\mathbb{D}$ bisimulation.

2. $\phi(x)$ is $\mathbb{C}$-invariant under $\mathbb{D}\ell$-bisimulation for some $\ell \in \mathbb{N}$.

3. $\phi(x)$ is equivalent to an $\mathcal{ALC}(\mathbb{D})$ concept.

Recall that the classes $C_{\text{all}}$, $C_{\text{fb}}$ and $C_{\text{fin}}$ satisfy the assumptions of Theorem 7. We further remark that, in contrast to the case of $\mathcal{ALCSCC}$, where there are concepts that are not FOL-definable, every $\mathcal{ALC}(\mathbb{D})$ concept is FOL($\mathbb{D}$)-definable.
# 5 Conclusion

We have investigated the expressive power of concept description languages that allow their users to employ numerical constraints when defining concepts in two orthogonal ways. In contrast to our previous results on the expressive power of such languages [7–10], the approach employed here also works for restricted classes of interpretations such as finitely branching or finite ones. In [8], we have characterized the expressive power of TBoxes and cardinality boxes of $ALCSCC^{\infty}$ (where arbitrary interpretations are considered) using global Pr bisimulations. It is at the moment not clear to us whether the results obtained there can be extended to the restricted classes of interpretations considered in the present paper. Another interesting topic for future research is to study the expressive power of $ALCOSCC(\mathcal{D})$, a joint extension of both $ALCSCC$ and $ALC(\mathcal{D})$, whose complexity has recently been analyzed in [5]. The DLs $ALCSCC$ and $ALC(\mathcal{D})$ are closed under all Boolean operations, whereas Kurtonina and de Rijke [20] characterize the expressive power of sub-Boolean fragments of $ALC$. It would be interesting to see whether their results can be extended to the corresponding fragments of $ALCSCC$ and $ALC(\mathcal{D})$. Like most bisimulation-based characterizations of the expressive power of logics, we assume here that the concept $D$ in the DL $\mathcal{L}_2$ expressing the concept $C$ in the DL $\mathcal{L}_1$ must be built over the same signature as $C$, i.e., no auxiliary symbols may be used. It would again be interesting to see whether inexpressivity results such as the one in Proposition 4 still hold if the use of auxiliary symbols is allowed, as for instance in [1,2]. In this context, work on conservative extensions could become relevant [16].

**Acknowledgments.** This work was partially supported by DFG grant 389792660 as part of TRR 248 – CPEC, by the German Federal Ministry of Education and Research (BMBF, SCADS22B) and the Saxon State Ministry for Science, Culture and Tourism (SMWK) by funding the competence center for Big Data and AI “ScaDS.AI Dresden/Leipzig”.

# References

1. Baader, F.: A formal definition for the expressive power of knowledge representation languages. In: Proceedings of the 9th European Conference on Artificial Intelligence, ECAI 1990, pp. 53–58 (1990)

2. Baader, F.: A formal definition for the expressive power of terminological knowledge representation languages. J. Log. Comput. **6**(1), 33–54 (1996). https://doi.org/10.1093/LOGCOM/6.1.33

3. Baader, F.: A new description logic with set constraints and cardinality constraints on role successors. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 43–59. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_3

4. Baader, F., Bednarczyk, B., Rudolph, S.: Satisfiability and query answering in description logics with global and local cardinality constraints. In: ECAI 2020 – 24th European Conference on Artificial Intelligence, pp. 616–623. IOS Press (2020). https://doi.org/10.3233/FAIA200146
5. Baader, F., Borgwardt, S., De Bortoli, F., Koopmann, P.: Concrete domains meet expressive cardinality restrictions in description logics. In: Barrett, C., Waldmann, U. (eds.) CADE-30: 30th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science, vol. 15943, pp.676–695. Springer (2025). https://doi.org/10.1007/978-3-031-99984-0_35

6. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003). https://doi.org/10.1017/CBO9780511711787

7. Baader, F., De Bortoli, F.: On the expressive power of description logics with cardinality constraints on finite and infinite sets. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 203–219. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29007-8_12

8. Baader, F., De Bortoli, F.: Description logics that count, and what they can and cannot count. In: Kovacs, L., Korovin, K., Reger, G. (eds.) ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia. EPiC Series in Computing, vol. 68, pp. 1–25. EasyChair (2020). https://doi.org/10.29007/ltzn

9. Baader, F., De Bortoli, F.: The abstract expressive power of first-order and description logics with concrete domains. In: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024, pp. 754–761. Association for Computing Machinery, New York (2024). https://doi.org/10.1145/3605098.3635984

10. Baader, F., De Bortoli, F.: Logics with concrete domains: first-order properties, abstract expressive power, and (un)decidability. SIGAPP Appl. Comput. Rev. 24(3), 5–17 (2024). https://doi.org/10.1145/3699839.3699840

11. Baader, F., De Bortoli, F.: The Expressive Power of Description Logics with Numerical Constraints over Restricted Classes of Models (Extended Version). LTCS-Report 25-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany (2025). https://doi.org/10.25368/2025.126

12. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence, IJCAI 1991, pp. 452–457. Morgan Kaufmann (1991). http://ijcai.org/Proceedings/91-1/Papers/070.pdf

13. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017). https://doi.org/10.1017/9781139025355

14. Baader, F., Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. J. Autom. Reason. 66(3), 357–407 (2022). https://doi.org/10.1007/s10817-022-09626-2

15. Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artif. Intell. 82(1–2), 353–367 (1996). https://doi.org/10.1016/0004-3702(96)00004-5

16. Botoeva, E., Konev, B., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Inseparability and conservative extensions of description logic ontologies: a survey. In: Pan, J.Z., et al. (eds.) Reasoning Web 2016. LNCS, vol. 9885, pp. 27–89. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-49493-7_2

17. Calvanese, D.: Finite model reasoning in description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR 1996), pp. 292–303. Morgan Kaufmann (1996)
18. Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335–346. Morgan Kaufmann (1991)

19. Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_15

20. Kurtonina, N., de Rijke, M.: Expressiveness of concept expressions in first-order description logics. Artif. Intell. 107(2), 303–333 (1999). https://doi.org/10.1016/S0004-3702(98)00109-X

21. Lutz, C., Miličić, M.: A tableau algorithm for description logics with concrete domains and general TBoxes. J. Autom. Reason. 38(1), 227–259 (2007). https://doi.org/10.1007/s10817-006-9049-7

22. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: model-theoretic characterizations and rewritability. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 983–988. IJCAI/AAAI (2011). https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-169

23. Lutz, C., Sattler, U., Tendera, L.: The complexity of finite model reasoning in description logics. Inf. Comput. 199(1–2), 132–171 (2005). https://doi.org/10.1016/j.ic.2004.11.002

24. Otto, M.: Model theoretic methods for fragments of FO and special classes of (finite) structures. In: Esparza, J., Michaux, C., Steinhorn, C. (eds.) Finite and Algorithmic Model Theory, pp. 271–338. Cambridge University Press, Cambridge (2011). https://doi.org/10.1017/CBO9780511974960.007

25. Otto, M.: Graded modal logic and counting bisimulation (2023). http://arxiv.org/abs/1910.00039

26. de Rijke, M.: A note on graded modal logic. Stud. Logica. 64(2), 271–283 (2000). https://doi.org/10.1023/A:1005245900406

27. Rosen, E.: Modal logic over finite structures. J. Logic Lang. Inf. 6(4), 427–439 (1997). https://www.jstor.org/stable/40181601

28. van Benthem, J.: Modal correspondence theory. Ph.D. thesis, Mathematical Institute, University of Amsterdam, The Netherlands (1976)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_17.png" /></figure>
# Reasoning in OWL 2 EL with Hierarchical Concrete Domains

Francesco Kriegel<fnref n="1" />,<fnref n="2" />(✉) ID

**Abstract.** The *EL* family of description logics facilitates efficient polynomial-time reasoning and has been standardized as the profile OWL 2 EL of the Web Ontology Language. *EL* can represent and reason not only with symbolic knowledge but also with concrete knowledge expressed by numbers, strings, and other concrete datatypes. Such concrete domains must be convex to avoid introducing disjunctions "through the backdoor." However, existing concrete domains provide only limited utility. In order to overcome this issue, we introduce a novel form of concrete domains based on semi-lattices. They are convex by design and can thus be integrated into Horn-DLs such as *EL*. Moreover, they allow for FBoxes to express dependencies between concrete features. We describe four instantiations concerned with real intervals, 2D-polygons, regular languages, and graphs.

## 1 Introduction

Concrete domains can be integrated in description logics (DLs) in order to refer to concrete knowledge expressed by numbers, strings, and other concrete datatypes [7]. They have mainly been investigated with DLs that are not Horn, such as *ALC* and its extensions, regarding decidability and complexity [14, 18, 20, 49–51], reasoning procedures [26, 27, 50–52, 58], an algebraic characterization [12, 59], and their expressive power [3, 6].

For computationally tractable description logics, other conditions on the concrete domains than above must be imposed. Suitable for the *EL* family are p-admissible concrete domains [4]: through them it is not possible to introduce disjunction into the logical domain so that the DL part retains its Horn character and, moreover, they guarantee that reasoning involving both the logical and the concrete domain remains tractable. Concrete domains have also been integrated with DL-Lite [2].

Existing p-admissible concrete domains for *EL* provide only limited utility. Using the concrete domain $D_{Q,diff}$ [4], we could express with the concept inclusions $(sys \ge 140) \sqsubseteq Hypertension$ and $(dia \ge 90) \sqsubseteq Hypertension$ that a systolic blood pressure of 140 or higher indicates hypertension, as does a diastolic blood pressure of at least 90. Since the opposite relations $\le$ are not available to ensure convexity, neither non-elevated blood pressure (dia. < 120 and sys. < 70) nor

<footnote n="1">¹ Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany
francesco.kriegel@tu-dresden.de</footnote>

<footnote n="2">² Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI),
Dresden/Leipzig, Germany</footnote>
elevated blood pressure (dia. between 120 and 140, and sys. between 70 and 90) are expressible. Mixed inequalities <, ≤, >, and ≥ may be used under certain limitations which of them may occur in left-hand sides and, respectively, in right-hand sides of concept inclusions [53]. While this retains convexity of the concrete domain, reasoning is then rather impaired since the usual completion procedure is only complete for consistency and classification, but not for subsumption.

An algebraic characterization of p-admissible concrete domains has put forth a further concrete domain $D_{\mathcal{Q},\text{lin}}$, which supports linear combinations of numerical features [11, 13]. For instance, the concept inclusion $\top \sqsubseteq (\text{sys} - \text{dia} - \text{pp} = 0)$, where $-$ is the difference operation in real arithmetic, expresses that the pulse pressure is the difference between the systolic and the diastolic blood pressure. In the medical domain, the combined expressivity of $D_{\mathcal{Q},\text{diff}}$ and $D_{\mathcal{Q},\text{lin}}$ would be useful since then with the concept inclusion $\text{ICUPatient} \sqcap (\text{pp} > 50) \sqsubseteq \text{NeedsAttention}$ it could be expressed that intensive-care patients with a pulse pressure exceeding 50 need attention—but this combination is not convex anymore [1].

We introduce a novel form of concrete domains based on semi-lattices. A semi-lattice $(L, \leq, \wedge)$ consists of a set $L$, a partial order $\leq$, and a binary meet operation $\wedge$. The elements of $L$ are taken as concrete values, and $\leq$ is understood as an “information order,” i.e. $p \leq q$ means that $p$ is more specific than $q$, like a subsumption order between concepts. The meet operation $\wedge$ is used to combine two values $p$ and $q$ to their meet value $p \wedge q$, which is the most general value that is more specific than both $p$ and $q$. For instance, real intervals form a semi-lattice with subset inclusion $\subseteq$ as partial order and intersection $\cap$ as meet operation. With that, the statement $\text{NonElevatedBP} \equiv (\text{sys} \subseteq [0, 120)) \cap (\text{dia} \subseteq [0, 70))$ defines non-elevated blood pressure, where $[0, 120)$ and $[0, 70)$ are real intervals.

Our new *hierarchical concrete domains* are convex by design, simply because a general value of a feature (such as $\text{sys} \subseteq [0, 120)$) does not imply the disjunction of all more specific feature values (such as $\text{sys} \subseteq [0, 0]$, $\text{sys} \subseteq [1, 1]$, ..., $\text{sys} \subseteq [119, 119]$). Atomic feature values are supported nonetheless when these are available as atoms in the semi-lattice. For instance, a specific numerical value $p$ is represented by the singleton interval $[p, p]$ (which equals the one-element set $\{p\}$).

In addition, we introduce *FBoxes* consisting of *feature inclusions* that describe dependencies between features as well as aggregations of features. For instance, through the feature inclusion $\text{pp} \subseteq \text{sys} - \text{dia}$, where $-$ is the difference operation in real interval arithmetic, we can obtain an interval value of the pulse pressure given intervals of the systolic and the diastolic blood pressure. With the concept inclusion $\text{ICUPatient} \sqcap (\text{pp} \subseteq (50, \infty)) \sqsubseteq \text{NeedsAttention}$ we can now express that intensive-care patients having a pulse pressure above 50 need attention and, unlike in the combination of $D_{\mathcal{Q},\text{diff}}$ and $D_{\mathcal{Q},\text{lin}}$, computationally reason with that in polynomial time.

We provide four instantiations of hierarchical concrete domains based on real intervals, 2D-polygons, regular languages, and graphs. The former two are not only convex, but indeed p-admissible, i.e. equipping a DL from the $\mathcal{EL}$ family with them facilitates polynomial-time reasoning. In particular, we can employ linear programming for reasoning in the interval domain when the FBox is affine.
The regular-language domain is also convex (again, by design) but requires exponential time for reasoning. However, this only affects the concrete-domain reasoning itself so that reasoning in the logical $\mathcal{EL}$ part still runs in polynomial time. This holds similarly for the graph domain.

Of practical relevance is that our hierarchical concrete domains can be seamlessly integrated into the completion procedure and the ELK reasoner [4, 5, 40, 42]. We demonstrate this for the case where nominals must be used safely, i.e. nominals must not occur in conjunctions and right-hand sides of concept inclusions must not be single nominals. We conjecture that full support for nominals can be achieved in the same way as without concrete domains [41].

Proofs and more technical details can be found in the extended version [46].

## 2 Preliminaries

We work with the description logic $\mathcal{EL}^{++}[\mathcal{D}]$ (OWL 2 EL) where $\mathcal{D}$ is a P-admissible concrete domain (as defined below). Consider a set C of atomic concepts, a set R of roles, a set I of individuals, a set F of features, and a set P of predicates where each $P \in P$ has an arity $\mathbf{ar}(P) \in \mathbb{N}$. There are two special concepts $\perp$ and $\top$ with fixed meaning. A constraint has the form $\exists f_1, ..., f_k.P$ where P is a k-ary predicate and $f_1, ..., f_k$ are features. Compound concepts are built by

$$C ::= \perp \mid \top \mid \{i\} \mid A \mid \exists f_1, ..., f_k.P \mid C \sqcap C \mid \exists r.C$$

where A ranges over all atomic concepts, r over all roles, i over all individuals, and $\exists f_1, ..., f_k.P$ over all constraints. A knowledge base (KB) is a finite set of concept inclusions (CIs) $C \subseteq D$ concerning concepts C and D, role inclusions (RIs) $R \sqsubseteq s$ involving role chains generated by $R ::= \varepsilon \mid R_1, R_1 ::= r \mid R_1 \circ R_1$ and roles s, and range inclusions $\mathbf{Ran}(r) \subseteq C$ referring to roles r and concepts C—but every $\mathcal{EL}^{++}[\mathcal{D}]$ KB must satisfy an additional condition as explained in Sect. 4.

As syntactic sugar, we have concept assertions $\{i\} \sqsubseteq C$ (also written $i: C$), role assertions $\{i\} \sqsubseteq \exists r.\{j\}$ (also written $(i, j): r$), domain inclusions $\exists r.\top \sqsubseteq C$ (also written $\mathbf{Dom}(r) \sqsubseteq C$), and role exclusions $\exists r_1. \dots \exists r_n. \top \sqsubseteq \perp$ (also written $r_1 \circ \dots \circ r_n \sqsubseteq \perp$). Statements $C \sqsubseteq \perp$ are also called concept exclusions, and $C \equiv D$ is a concept equivalence that stands for the two CIs $C \sqsubseteq D$ and $D \sqsubseteq C$. Each KB $\mathcal{K}$ can be subdivided into an ABox $\mathcal{A}$ consisting of all concept and role assertions, an RBox $\mathcal{R}$ consisting of all role inclusions and exclusions, and a TBox $\mathcal{T}$ consisting of the remaining statements. The TBox together with the RBox is also called an ontology $\mathcal{O}$.

The semantics are defined through the fixed concrete domain $\mathcal{D}$ and all interpretations $\mathcal{I}$. The concrete domain $\mathcal{D} := (\mathbf{Dom}(\mathcal{D}), \cdot^{\mathcal{D}})$ consists of a set $\mathbf{Dom}(\mathcal{D})$ of values and an interpretation function $\cdot^{\mathcal{D}}$ that sends each predicate $P \in P$ to a relation over $\mathbf{Dom}(\mathcal{D})$ with arity $\mathbf{ar}(P)$, i.e. $P^{\mathcal{D}} \subseteq \mathbf{Dom}(\mathcal{D})^{\mathbf{ar}(P)}$.

If the predicate P in a constraint $\exists f_1, ..., f_k.P$ is defined through a mathematical expression or a logical formula with k free variables, then we may
represent the constraint also through this expression/formula but with the free variables replaced by the features $f_1, \dots, f_k$. For instance, the constraint $\mathbf{sys} - \mathbf{dia} - \mathbf{pp} = 0$ from the introduction represents $\exists \mathbf{sys}, \mathbf{dia}, \mathbf{pp}. P_{(1,-1,-1),0}$ where $(P_{(1,-1,-1),0})^D := \{(x, y, z) \mid x - y - z = 0\}$.

An interpretation $\mathcal{I} := (\mathrm{Dom}(\mathcal{I}), \mathcal{I}^I)$ consists of a non-empty set $\mathrm{Dom}(\mathcal{I})$, called *domain*, and an interpretation function $\mathcal{I}^I$ that maps each atomic concept $A \in \mathbf{C}$ to a subset $A^I$ of $\mathrm{Dom}(\mathcal{I})$, each role $r \in \mathbf{R}$ to a binary relation $r^I$ over $\mathrm{Dom}(\mathcal{I})$, each individual $i \in \mathbf{I}$ to an element $i^I$ of $\mathrm{Dom}(\mathcal{I})$, and each feature $f \in \mathbf{F}$ to a partial function $f^I$ from $\mathrm{Dom}(\mathcal{I})$ to $\mathrm{Dom}(\mathcal{D})$. The interpretation function $\mathcal{I}^I$ is extended to compound concepts as follows: $\perp^I := \emptyset$, $\top^I := \mathrm{Dom}(\mathcal{I})$, $\{i\}^I := \{i^I\}$, $(\exists f_1, \dots, f_k. P)^I := \{x \mid x \in \mathrm{Dom}(f_1^I) \cap \dots \cap \mathrm{Dom}(f_k^I) \text{ and } (f_1^I(x), \dots, f_k^I(x)) \in P^D\}$, $(C \sqcap D)^I := C^I \cap D^I$, and $(\exists r. C)^I := \{x \mid \text{there is } y \text{ s.t. } (x, y) \in r^I \text{ and } y \in C^I\}$. Role chains are interpreted by $\varepsilon^I := \{(x, x) \mid x \in \mathrm{Dom}(\mathcal{I})\}$ and $(R \circ S)^I := \{(x, z) \mid \text{there is } y \text{ s.t. } (x, y) \in R^I \text{ and } (y, z) \in S^I\}$, and role ranges are interpreted as $\mathrm{Ran}(r)^I := \{y \mid \text{there is } x \text{ s.t. } (x, y) \in r^I\}$.

$\mathcal{I}$ satisfies a concept/role/range inclusion $X \sqsubseteq Y$, written $\mathcal{I} \models X \sqsubseteq Y$, if $X^I \subseteq Y^I$. If $\mathcal{I}$ satisfies all inclusions in a KB $\mathcal{K}$, then $\mathcal{I}$ is a *model of* $\mathcal{K}$, written $\mathcal{I} \models \mathcal{K}$. If $\mathcal{K}$ has a model, then it is *consistent*, and otherwise *inconsistent*. $\mathcal{K}$ *entails* an inclusion $X \sqsubseteq Y$ if $X \sqsubseteq Y$ is satisfied by all models of $\mathcal{K}$, written $\mathcal{K} \models X \sqsubseteq Y$ or $X \sqsubseteq^K Y$, and we then say that $X$ is *subsumed by* $Y$ w.r.t. $\mathcal{K}$. Furthermore, $\mathcal{K}$ *entails* a KB $\mathcal{L}$ if $\mathcal{K}$ entails all inclusions in $\mathcal{L}$, written $\mathcal{K} \models \mathcal{L}$.

A constraint inclusion is of the form $\bigcap \Gamma \sqsubseteq \sqcup \Delta$ where $\Gamma$ and $\Delta$ are finite sets of constraints. $\mathcal{I}$ satisfies $\bigcap \Gamma \sqsubseteq \sqcup \Delta$, written $\mathcal{I} \models \bigcap \Gamma \sqsubseteq \sqcup \Delta$, if $\bigcap \{\alpha^I \mid \alpha \in \Gamma\} \subseteq \bigcup \{\beta^I \mid \beta \in \Delta\}$. Moreover, $\bigcap \Gamma \sqsubseteq \sqcup \Delta$ is valid, written $\mathcal{D} \models \bigcap \Gamma \sqsubseteq \sqcup \Delta$, if it is satisfied in all interpretations. It is easy to see that validity is independent of the concepts, roles, and individuals and that it suffices to consider only one domain element. To this end, a valuation is a partial function $v$ from $\mathbf{F}$ to $\mathrm{Dom}(\mathcal{D})$, and it satisfies $\exists f_1, \dots, f_k. P$ if $(v(f_1), \dots, v(f_k)) \in P^D$. Now, $\bigcap \Gamma \sqsubseteq \sqcup \Delta$ is valid iff., for each valuation $v$, if $v$ satisfies all $\alpha \in \Gamma$, then $v$ satisfies some $\beta \in \Delta$.

We say that $\mathcal{D}$ is P-admissible if satisfiability of constraint conjunctions as well as validity of constraint inclusions are decidable in polynomial time and, moreover, $\mathcal{D}$ is convex, i.e. for each valid constraint inclusion $\bigcap \Gamma \sqsubseteq \sqcup \Delta$, there is a constraint $\beta \in \Delta$ such that $\bigcap \Gamma \sqsubseteq \beta$ is valid. We can use multiple P-admissible concrete domains by forming their disjoint union, which is P-admissible too.

## 3 Hierarchical Concrete Domains

A semi-lattice $\mathbf{L} := (L, \leq, \wedge)$ consists of a set $L$, a partial order $\leq$ on $L$, and a binary meet operation $\wedge$ on $L$, i.e. the following hold for all $p, q, p_1, p_2, p_3 \in L$:

(SL1) $p \leq p$ for each $p \in L$ (reflexive)

(SL2) if $p \leq q$ and $q \leq p$, then $p = q$ (anti-symmetric)

(SL3) if $p_1 \leq p_2$ and $p_2 \leq p_3$, then $p_1 \leq p_3$ (transitive)

(SL4) $p_1 \wedge p_2 \leq p_1$ and $p_1 \wedge p_2 \leq p_2$

(SL5) if $q \leq p_1$ and $q \leq p_2$, then $q \leq p_1 \wedge p_2$.
The strict part < is defined by $p < q$ if $p \le q$ but $q \not\le p$, and we then say that $p$ is more specific than $q$. Thus $p \le q$ iff. $p < q$ or $p = q$, in which case we say that $p$ is more specific than or equal to $q$. And $p \wedge q$ is the meet of $p$ and $q$. It follows from the above conditions that $\wedge$ is associative, commutative, and idempotent. The finitary meet operation $\wedge$ is obtained from the binary one by setting $\wedge\{p\} := p$, $\wedge\{p, q\} := p \wedge q$, and $\wedge\{p_1, \dots, p_n\} := p_1 \wedge \wedge\{p_2, \dots, p_n\}$ whenever $n \ge 3$.

We say that $\mathbf{L}$ is *computable* if $L$ and $\le$ are decidable and $\wedge$ is computable. If all this is possible in polynomial time, then $\mathbf{L}$ is *polynomial-time computable*. $\mathbf{L}$ is *bounded* if it has a greatest element $\top$, i.e. $p \le \top$ for every $p \in L$. Then we can also define a nullary meet as $\wedge\emptyset := \top$. In order to express impossible combinations of values, it might be convenient to add an artificial smallest element $\bot$ to the semi-lattice, i.e. $\bot \le p$ for each $p \in L$. We then use $\bot$ to represent contradictory or ill-defined values. More specifically, $p \wedge q = \bot$ if it is impossible to combine the values $p$ and $q$.

**Example 1.** A semi-lattice representing grades could have the values *Attended*, *Passed*, *Failed*, 1, 2, 3, 4, 5, 6, 1.0, 1.3, 1.7, 2.0, and so on. Its partial order $\le$ is defined by $\text{Passed} \le \text{Attended}$, $\text{Failed} \le \text{Attended}$, $1 \le \text{Passed}$, $2 \le \text{Passed}$, $3 \le \text{Passed}$, $4 \le \text{Passed}$, $5 \le \text{Failed}$, $6 \le \text{Failed}$, $1.0 \le 1$, $1.3 \le 1$, $1.7 \le 2$, $2.0 \le 2$, etc. Here we need to add a smallest element $\bot$ since e.g. the meet of grades 1.0 and 5.0 cannot be reasonably defined.

For every KB $\mathcal{K}$ expressed in a decidable DL, the set of all concepts ordered by subsumption $\sqsubseteq^K$ and with conjunction $\sqcap$ as meet operation is a computable, bounded semi-lattice. For each set $M$, $(\wp(M), \subseteq, \cap, M)$ and $(\wp(M), \supseteq, \cup, \emptyset)$ are bounded semi-lattices (where $\wp(M)$ is the powerset of $M$). They are only computable if restricted to finite or finitely representable subsets of $M$. In the following subsections we will introduce four application-relevant semi-lattices based on intervals, polygons, regular languages, and graphs.

**Definition 2.** Given a bounded semi-lattice $\mathbf{L} := (L, \leq, \wedge, \top)$, the hierarchical concrete domain $\mathcal{D}_{\mathbf{L}}$ has values in $\text{Dom}(\mathcal{D}_{\mathbf{L}}) := L$ and supports only constraints of the form $\exists f.P_{\leq p}$, written as $f \le p$, involving a feature $f$ and a value $p$. The semantics are $(P_{\leq p})^{\mathcal{D}_{\mathbf{L}}} := \{q | q \in L \text{ and } q \le p\}$ and thus $(f \le p)^{\mathcal{I}} = \{x | f^{\mathcal{I}}(x) \le p\}$. Recall: this means that $f$'s value is $p$ or more specific, not smaller. We assume that $\top$ stands for an undefined value and thus all valuations are total, i.e. $v(f) = \top$ means that $f$ has no value under $v$. In order to represent a most general value, $\mathbf{L}$ contains a second-largest element $\Box$, i.e. $\Box < \top$ and $p \le \Box$ for each $p \in L \setminus \{\top\}$. Since $\bot$ represents contradictory, ill-defined values, no valuation $v$ assigns $\bot$ to any feature $f$, i.e. $v(f) \ne \bot$.

**Definition 3.** A feature inclusion (FI) $f \le H(g_1, \dots, g_n)$ consists of features $f, g_1, \dots, g_n$ and a computable $n$-ary operation $H: L^n \to L$ that is monotonic in the sense that $H(p_1, \dots, p_n) \le H(q_1, \dots, q_n)$ whenever $p_1 \le q_1, \dots, p_n \le q_n$ (i.e. applying $H$ to more specific values yields more specific values). A valuation $v$ satisfies this FI if $v(f) \le H(v(g_1), \dots, v(g_n))$, denoted as $v \models f \le H(g_1, \dots, g_n)$. An FBox $\mathcal{F}$ is a finite set of FIs, and a valuation $v$ satisfies
F, written $v \models F$, if $v$ satisfies every FI in $F$. We call $F$ acyclic if the graph $(\mathbf{F}, \{(f, g_1), \dots, (f, g_n) | f \le H(g_1, \dots, g_n) \in F\})$ is, and cyclic otherwise.

The following example illustrates that FIs are “directed specifications” in the sense that values of the right-hand side features $g_1, \dots, g_n$ yield, through the operation $H$, an upper bound for the value of the left-hand side feature $f$. However, this does not work in the other direction unless specified by other FIs.

**Example 4.** We use three features with interval values over the non-negative integers: **sys** for the systolic and **dia** for the diastolic blood pressure, and **pp** for the pulse pressure, which is the difference between the systolic and the diastolic pressure. The FI $\mathbf{pp} \subseteq \mathbf{sys} - \mathbf{dia}$ allows us to infer a value for **pp** when values for both **sys** and **dia** are given. The monotonic operator $H$ in the right-hand side is $H([p_1, q_1], [p_2, q_2]) := [p_1, q_1] - [p_2, q_2]$, and the latter value is the difference in interval arithmetic ($= [p_1 - q_2, q_1 - p_2]$ but with negative subtraction results replaced by 0). According to the semantics, an interval value of the feature **pp** must be a subset of **sys** - **dia**, i.e. if the latter two features are defined for an object $x$ in a model $\mathcal{I}$ of the FI, then also $\mathbf{pp}^{\mathcal{I}}(x)$ is defined and is equal to or more specific than $H(\mathbf{sys}^{\mathcal{I}}(x), \mathbf{dia}^{\mathcal{I}}(x))$.

For instance, under the above FI the constraint inclusion $(\mathbf{sys} \subseteq [110, 120]) \sqcap (\mathbf{dia} \subseteq [60, 70]) \subseteq (\mathbf{pp} \subseteq [40, 60])$ is valid since $H([110, 120], [60, 70]) = [40, 60] \subseteq [40, 60]$. Without syntactic sugar, the first constraint is $\exists \mathbf{sys.} P_{\subseteq [110, 120]}$ involving the predicate $P_{\subseteq [110, 120]} := \{[p, q], (p, q), [p, q], (p, q] | 110 \le p \le q \le 120\}$.

In contrast, the constraint inclusion $(\mathbf{sys} \subseteq [110, 120]) \sqcap (\mathbf{pp} \subseteq [40, 60]) \supseteq (\mathbf{dia} \subseteq [60, 70])$ is not valid w.r.t. the above FI. A countervalueation is $v$ with $v(\mathbf{sys}) = [110, 120]$, $v(\mathbf{dia}) = [0, \infty)$, $v(\mathbf{pp}) = [40, 60]$. This is because $[110, 120] - [0, \infty) = [0, 120]$ and $[40, 60] \subseteq [0, 120]$, i.e. $v$ satisfies the FI, but $v$ does not satisfy the latter constraint inclusion.

**Definition 5.** The semantics of the concrete domain $\mathcal{D}_L$ can be restricted w.r.t. an FBox $\mathcal{F}$ by considering only valuations satisfying $\mathcal{F}$. That is, a constraint inclusion $\sqcap \Gamma \subseteq \sqcup \Delta$ is valid in $\mathcal{D}_L$ w.r.t. $\mathcal{F}$, written $\mathcal{D}_L, \mathcal{F} \models \sqcap \Gamma \subseteq \sqcup \Delta$, if this inclusion is satisfied in all valuations that satisfy $\mathcal{F}$. Whenever we write "w.r.t. $\mathcal{F}$" in the following, only valuations satisfying $\mathcal{F}$ are considered.

Using this semantics restricted by an FBox, convexity and P-admissibility are defined as before but the latter additionally takes the FBox $\mathcal{F}$ as part of the input. The underlying semi-lattice $\mathbf{L}$ is taken into account through the computational complexity of its value set $L$, its partial order $\leq$, and its meet operation $\wedge$.

**Definition 6.** $\mathcal{D}_L$ is admissible w.r.t. $\mathcal{F}$ if $\mathcal{D}_L$ is convex and satisfiability of constraint conjunctions as well as validity of constraint inclusions are decidable, all w.r.t. $\mathcal{F}$. For a complexity class $C$, we say that $\mathcal{D}_L$ is C-admissible w.r.t. $\mathcal{F}$ if, all w.r.t. $\mathcal{F}$, $\mathcal{D}_L$ is convex and satisfiability of constraint conjunctions as well as validity of constraint inclusions are in $C$ when $\mathcal{F}$ is part of the input.

Next, we show that a hierarchical concrete domain $\mathcal{D}_L$ is convex w.r.t. $\mathcal{F}$ if the semi-lattice $\mathbf{L}$ is complete or well-founded or the FBox $\mathcal{F}$ is acyclic. There might be further sufficient conditions for convexity; we leave this for future research.
**Definition 7.** Let $\mathbf{L}$ be a bounded semi-lattice and $\mathcal{F}$ be an FBox. Given a finite set $\Gamma$ of constraints over the concrete domain $\mathcal{D}_{\mathbf{L}}$, a canonical valuation of $\Gamma$ w.r.t. $\mathcal{F}$ is a valuation $v_{\Gamma, \mathcal{F}}$ such that

1. $v_{\Gamma, \mathcal{F}} \models \mathcal{F}$ and

2. $v_{\Gamma, \mathcal{F}} \models \alpha$ iff. $\mathcal{D}_{\mathbf{L}}, \mathcal{F} \models \bigcap \Gamma \subseteq \alpha$ for each constraint $\alpha$.

Moreover, we say that $\mathcal{D}_{\mathbf{L}}$ has canonical valuations w.r.t. $\mathcal{F}$ if such a valuation $v_{\Gamma, \mathcal{F}}$ exists for every finite, w.r.t. $\mathcal{F}$ satisfiable $\Gamma$.

Since for each constraint $\alpha$ in $\Gamma$, the inclusion $\bigcap \Gamma \subseteq \alpha$ is valid, we infer with the second condition that $v_{\Gamma, \mathcal{F}}$ satisfies $\Gamma$.

A semi-lattice $\mathbf{L}$ is complete if every subset $P \subseteq L$ has a meet $\bigwedge P \in L$, i.e. such that $\bigwedge P \le p$ for each $p \in P$ and, if $q \le p$ for each $p \in P$, then $q \le \bigwedge P$. Note that these two conditions generalize (SL4) and (SL5).

**Theorem 8.** For each complete semi-lattice $\mathbf{L}$ and for every FBox $\mathcal{F}$, the concrete domain $\mathcal{D}_{\mathbf{L}}$ has canonical valuations and so is convex w.r.t. $\mathcal{F}$.

**Theorem 9.** Let $\mathbf{L}$ be a computable, bounded semi-lattice and $\mathcal{F}$ be an FBox. If $\mathbf{L}$ is well-founded or $\mathcal{F}$ is acyclic, then the concrete domain $\mathcal{D}_{\mathbf{L}}$ has computable canonical valuations and is admissible w.r.t. $\mathcal{F}$.

Now, we want to determine the time requirement for computing a canonical valuation $v_{\Gamma, \mathcal{F}}$, which is measured w.r.t. the constraint set $\Gamma$ and the FBox $\mathcal{F}$.

An operation $H: L^n \rightarrow L$ is *non-duplicating* if, for all $(p_1, \dots, p_n) \in L^n$, the size of $H(p_1, \dots, p_n)$ is no larger than the size of $(p_1, \dots, p_n)$. An FBox is *non-duplicating* if all operations in it are non-duplicating and each feature occurs at most once in any right-hand side.

**Proposition 10.** Consider a polynomial-time computable, bounded semi-lattice $\mathbf{L}$ such that its meet operation is non-duplicating. Further consider an acyclic, non-duplicating FBox $\mathcal{F}$ in which all occurring operations are polynomial-time computable. W.r.t. $\mathcal{F}$, the concrete domain $\mathcal{D}_{\mathbf{L}}$ has polynomial-time computable canonical valuations and is P-admissible.

We obtain exponential complexity if $\wedge$ and $\mathcal{F}$ are not non-duplicating.

**Proposition 11.** For every polynomial-time computable, bounded semi-lattice $\mathbf{L}$ and for every acyclic FBox $\mathcal{F}$ in which all occurring operations are polynomial-time computable, the concrete domain $\mathcal{D}_{\mathbf{L}}$ has exponential-time computable canonical valuations and is EXP-admissible w.r.t. $\mathcal{F}$.

## 3.1 Intervals

Let $N$ be a non-empty set of real numbers. The semi-lattice $\text{Int}(N)$ consists of all intervals over $N$, is partially ordered by set inclusion $\subseteq$ and has set intersection $\cap$ as its meet operation. $\text{Int}(N)$ is already bounded since its greatest element is $N = (-\infty, \infty)$, but we rather identify it with $\emptyset$ and add an artificial greatest
element $\top$. It also has a smallest element $\emptyset = (p, p)$ where $p \in N$ is arbitrary, and we identify this smallest element with the contradictory value $\bot$. The inclusion satisfies $[p_1, q_1] \subseteq [p_2, q_2]$ iff. $p_2 \le p_1$ and $q_1 \le q_2$, and the intersection satisfies $[p_1, q_1] \cap [p_2, q_2] = [\max(p_1, p_2), \min(q_1, q_2)]$, and similarly for the other interval types. It follows that $\mathbf{Int}(N)$ is polynomial-time computable since $\le$ is decidable in polynomial time [30], and its meet operation is non-duplicating.

The hierarchical concrete domain $\mathcal{D}_{\mathbf{Int}(N)}$ is called the *interval domain* over $N$. Since for every number $p \in N$, the singleton $\{p\}$ equals the interval $[p, p]$, we can specify the precise numerical value of a feature with the constraint $f \subseteq \{p\}$, also written $f = p$. Moreover, instead of $f \subseteq [p, q]$ we may also write $p \le f \le q$.

**Example 12.** Through the interval domain over the non-negative 8-bit integers $N := \mathbb{N} \cap [0, 2^8 - 1]$ we could express non-elevated blood pressure by $\text{NonElevatedBP} \equiv (\text{sys} \subseteq [0, 120)) \cap (\text{dia} \subseteq [0, 70))$, elevated blood pressure by $\text{ElevatedBP} \equiv (\text{sys} \subseteq [120, 140)) \cap (\text{dia} \subseteq [70, 90))$, and hypertension by $(\text{sys} \subseteq [140, \infty)) \sqsubseteq (\text{Hypertension} \text{ and } (\text{dia} \subseteq [90, \infty)) \sqsubseteq (\text{Hypertension})$. With the above syntactic sugar, the first statement can also be written as $\text{NonElevatedBP} \equiv (0 \le \text{sys} < 120) \cap (0 \le \text{dia} < 70)$, and similarly for the other two. The concrete values of patient *bob* can be represented by the assertions $\text{bob} : (\text{sys} = 114)$ and $\text{bob} : (\text{dia} \subseteq [69, 69])$. The KB consisting of all these aforementioned statements entails $\text{bob} : \text{NonElevatedBP}$.

**Example 13.** Continuing Example 4, we can additionally consider the two FIs $\text{dia} \subseteq \text{sys} - \text{pp}$ and $\text{sys} \subseteq \text{dia} + \text{pp}$, which allow us to also infer interval values of $\text{dia}$ and $\text{sys}$ given interval values of the respective other two. Importantly, this does not destroy convexity.

This is in stark contrast to the concrete domain extending $\mathcal{D}_{\mathbb{Q},\text{diff}}$ with constraints $f \ge b$, $f < b$, $f \le b$, which allows to express interval values as well (in a different way though). There, the constraint inclusion $(\text{sys} - \text{dia} = 40) \subseteq (\text{sys} \le 120) \sqcup (\text{dia} > 80)$ is valid, violating convexity. Additionally using the expressivity of $\mathcal{D}_{\mathbb{Q},\text{lin}}$, we could express that $\text{pp} = \text{sys} - \text{dia}$ by the CI $\top \sqsubseteq (\text{sys} - \text{dia} - \text{pp} = 0)$ as in Example 3 in [1]. Under this CI, the constraint inclusion $(\text{pp} = 40) \sqsubseteq (\text{sys} \le 120) \sqcup (\text{dia} > 80)$ would be valid, also violating convexity.

In our interval domain over the non-negative integers and with the cyclic FBox $\{\text{pp} \subseteq \text{sys} - \text{dia}, \text{dia} \subseteq \text{sys} - \text{pp}, \text{sys} \subseteq \text{dia} + \text{pp}\}$, the similar constraint inclusion $(\text{pp} \subseteq [40, 40)) \sqsubseteq (\text{sys} \subseteq [0, 120)) \sqcup (\text{dia} \subseteq (80, \infty))$ is not valid. A countervaluation is $v$ where $v(\text{sys}) = [40, \infty)$, $v(\text{dia}) = [0, \infty)$, $v(\text{pp}) = [40, 40]$. It satisfies the first FI since $[40, \infty) - [0, \infty) = [0, \infty) \supseteq [40, 40]$, the second FI since $[40, \infty) - [40, 40] = [0, \infty) \supseteq [0, \infty)$, and the third FI since $[0, \infty) + [40, 40] = [40, \infty) \supseteq [40, \infty)$.

Recall that the interval semi-lattice $\mathbf{Int}(N)$ is defined for every non-empty set $N$ of real numbers. The set $N$ is partially ordered by the usual ordering $\le$ and has the meet operation $\text{min}$, i.e. $(N, \le, \text{min})$ is itself a semi-lattice. It thus makes sense to say that $N$ is complete. The real numbers $\mathbb{R}$, the non-negative real numbers $\mathbb{R}_+$, the integers $\mathbb{Z}$, the natural numbers $\mathbb{N}$, the $n$-bit integers, the $n$-bit floating-point numbers, the $n$-bit fixed-point numbers, and all finite subsets of $\mathbb{R}$ are complete, but the rational numbers $\mathbb{Q}$ is not—for instance, the infimum
of $\{(1 + 1/n)^{n+1} | n \ge 0\}$ is Euler's number $e$, an irrational number. It is easy to see that the semi-lattice $\mathbf{Int}(N)$ is complete if the number set $N$ is complete, and so we obtain the below corollary to Theorem 8.

**Corollary 14.** If the semi-lattice $(N, \leq, \min)$ is complete, then the interval domain $\mathcal{D}_{\mathbf{Int}(N)}$ has canonical valuations and is convex w.r.t. every FBox $\mathcal{F}$.

An immediate consequence of Theorem 9 is that the interval domain $\mathcal{D}_{\mathbf{Int}(\mathbb{R})}$ over all real numbers is admissible w.r.t. every acyclic FBox. Moreover, an obvious corollary to Proposition 10 is as follows.

**Corollary 15.** W.r.t. each acyclic, non-duplicating FBox $\mathcal{F}$ in which all operations are polynomial-time computable, the interval domain $\mathcal{D}_{\mathbf{Int}(\mathbb{R})}$ has polynomial-time-computable canonical valuations and is P-admissible.

Next, we employ linear programming to handle affine FBoxes, which might be cyclic. We call an FBox $\mathcal{F}$ affine if all operations in FIs in $\mathcal{F}$ are affine, i.e. all FIs are of the form $f \subseteq \sum_{i=1}^n P_i \cdot g_i + Q_i$ where the $P_i$ and $Q_i$ are intervals. For instance, the FI $pp \subseteq \text{sys} - \text{dia}$ is affine, but $\text{bmi} \subseteq \text{bodyMass}/\text{bodyHeight}^2$ is not. Since each affine FI represents two linear inequalities (one for the lower bound of the interval value of $f$, and another one for the upper bound), we can transform affine FBoxes into linear programs, which can be solved in polynomial time [33]. We thus obtain the following result.

**Proposition 16.** Let $c, \bar{c} \in \mathbb{R}_+$ be non-negative real numbers such that $c \le \bar{c}$. Restricted to closed intervals only, the interval domain $\mathcal{D}_{\mathbf{Int}([c, \bar{c}]})$ over the non-negative real numbers between $c$ and $\bar{c}$ is P-admissible w.r.t. each affine FBox $\mathcal{F}$, i.e. all FIs are of the form $f \subseteq \sum_{i=1}^n [a_i, \bar{a}_i] \cdot g_i + [b, \bar{b}]$.

It remains an open problem, whether the interval domains $\mathcal{D}_{\mathbf{Int}([c, \bar{c}]})$ remain P-admissible w.r.t. affine FBoxes when all interval types would be considered. We conjecture that the interval bounds can be computed using the same linear program, but determining the correct interval types (closed or open at the lower bound, closed or open at the upper bound) could possibly lead to a combinatorial explosion. It is further unclear whether, without the bounding interval $[c, \bar{c}]$, the interval domain $\mathcal{D}_{\mathbf{Int}(\mathbb{R}_+)}$ would still be P-admissible w.r.t. affine FBoxes. The canonical valuation could then send features to intervals with upper bound $+\infty$, in which case the polytope described by the inequations would be unbounded. This requires an LP-solver with support for unbounded solution polytopes.

We can also handle affine FBoxes together with negative numbers, but then need to restrict the coefficient intervals $[a_i, \bar{a}_i]$ to singletons—as otherwise the non-linear functions min and max would be required to compute a product $[a_i, \bar{a}_i] \cdot g_i$, i.e. the system of inequalities would not be linear anymore and could therefore not be solved by linear-programming methods.

**Proposition 17.** Let $c, \bar{c} \in \mathbb{R}$ be real numbers such that $c \le \bar{c}$. Restricted to closed intervals, the interval domain $\mathcal{D}_{\mathbf{Int}([c, \bar{c}]})$ over the real numbers in $[c, \bar{c}]$ is P-admissible w.r.t. each affine FBox $\mathcal{F}$ involving only singleton coefficients, i.e. all FIs are of the form $f \subseteq \sum_{i=1}^n \{a_i\} \cdot g_i + [b, \bar{b}]$.
Linear programming becomes NP-hard when restricted to integers only [38]. Unless $P = NP$, the integer interval domains $D_{Int(Z)}$, $D_{Int(N)}$, and $D_{Int(\{0,1\})}$ are thus not P-admissible w.r.t. affine FBoxes. These domains are rather suitable for integration into Horn logics [55] that do not allow for polynomial-time reasoning, such as *ELI* [4], *Horn-ALC* [47], *Horn-SROIQ* [57], and existential rules [15].

*Example 18.* Example 3 in [1] shows that the combination of the concrete domains $D_{Q,diff}$ and $D_{Q,lin}$ is not enough to express that intensive-care patients need attention if their pulse pressure is larger than 50 or their current heart rate exceeds their maximal heart rate. Moreover, this combination is not even convex.

With our interval domain these statements can be expressed through the affine FIs $pp \subseteq sys - dia$, and $maxHR \subseteq 220 - age$, and $exceedHR \subseteq hr - maxHR$, as well as the CIs $ICUPatient \sqsubseteq (hr \sqsubseteq \square) \sqcap (sys \sqsubseteq \square) \sqcap (dia \sqsubseteq \square)$, and $ICUPatient \sqcap (pp \subseteq (50, \infty)) \sqsubseteq NeedsAttention$, and $ICUPatient \sqcap (exceedHR \subseteq (0, \infty)) \sqsubseteq NeedsAttention$.

## 3.2 2D-Polygons

A 2D-polygon is a finite sequence of successively connected finite line segments in the real plane $\mathbb{R}^2$ such that the end vertex of the last segment equals the start vertex of the first. These line segments form a simple closed curve in $\mathbb{R}^2$, and by the Jordan Curve Theorem [28,36] each 2D-polygon has an *interior region* (bounded by the curve) and an *exterior region*. In the following we identify each 2D-polygon with the subset of $\mathbb{R}^2$ consisting of its boundary and the *interior region*. 2D-polygons are thoroughly studied in Computational Geometry and frequently used in geographic information systems (GIS).

Every 2D-polygon can be represented as a finite sequence of vertex coordinates in $\mathbb{R}^2$—its line segments then connect each two subsequent coordinates and, respectively, the first and last coordinate—and thus deciding the set of all 2D-polygons is trivial. Clipping algorithms allow for deciding in polynomial time if a polygon is a subset of another (i.e. polygon containment without moving or scaling operations) as well as for computing any Boolean operation involving two polygons (union, intersection, difference, xor) in polynomial time [24,54,63]. However, intersections can be of quadratic size and might consist of unions of disjoint 2D-polygons. In order to obtain a semi-lattice, which must be closed under its meet operation, it would therefore be necessary to take the set of all finite unions of separated 2D-polygons: we denote it by **UGon**($\mathbb{R}^2$), its partial order is containment $\subseteq$, and its meet is intersection $\cap$. According to the above references, **UGon**($\mathbb{R}^2$) is polynomial-time computable (w.r.t. arithmetic complexity). The hierarchical concrete domain $D_{UGon}(\mathbb{R}^2)$ is called *polygon domain* over $\mathbb{R}^2$. A corollary to Proposition 11 is as follows.

**Corollary 19.** W.r.t. *arithmetic complexity*, the *polygon domain* $D_{UGon}(\mathbb{R}^2)$ has exponential-time computable canonical valuations and is EXP-admissible w.r.t. each acyclic FBox $F$ in which all operations are polynomial-time computable.
To the best of the author’s knowledge, it is unclear whether the intersection of $n$ polygons might reach an exponential size. If this worst case would not be possible and, moreover, all operations in $\mathcal{F}$ are non-duplicating, then $\mathcal{D}_{\text{UGon}(\mathbb{R}^2)}$ would even be P-admissible w.r.t. $\mathcal{F}$ (w.r.t. arithmetic complexity).

*Example 20.* Locations can be represented as polygons in the real plane $\mathbb{R}^2$. For instance, we have “Nöthnitzer Straße 46, 01187 Dresden” $\subseteq$ “01187 Dresden” $\subseteq$ “Dresden” $\subseteq$ “Saxony” $\subseteq$ “Germany” $\subseteq$ “Europe” $\subseteq$ “Earth”.

The situation is computationally easier with *convex* 2D-polygons, which contain all line segments between each two of their points. One can think of convex 2D-polygons as two-dimensional generalizations of closed intervals. Both in linear time, we can decide the subset relation $\subseteq$ and compute the intersection operation $\cap$ for convex 2D-polygons [56, 60, 62]. Intersection is non-duplicating [60]. However, deciding the set of all convex 2D-polygons is not trivial anymore but needs linear time [60]. We denote the semi-lattice of all convex 2D-polygons by $\text{CGon}(\mathbb{R}^2)$, and it is linear-time computable (w.r.t. arithmetic complexity). The hierarchical concrete domain $\mathcal{D}_{\text{CGon}(\mathbb{R}^2)}$ is called *convex-polygon domain* over $\mathbb{R}^2$.

Obviously, convex polygons are closed under intersection but not under union, difference, and xor. Since union is monotonic, it can be used in FBoxes when followed by the convex-hull operation (which computes the smallest enclosing polygon that is convex). This is, however, not possible for difference and xor since they are not monotonic. Suitable monotonic operations besides intersection and convex union are translation, rotation, and scaling, and these can be computed in linear time as well. Below is a corollary to Proposition 10.

**Corollary 21.** *W.r.t. each acyclic, non-duplicating FBox $\mathcal{F}$ in which all occurring operations are polynomial-time computable, the convex-polygon domain $\mathcal{D}_{\text{CGon}(\mathbb{R}^2)}$ has polynomial-time computable canonical valuations and is P-admissible (w.r.t. arithmetic complexity).*

Contrary to $\text{Int}(\mathbb{R})$, neither $\text{UGon}(\mathbb{R}^2)$ nor $\text{CGon}(\mathbb{R}^2)$ are complete. One reason is that the unit circle can be obtained as the intersection of regular polygons (for each $n \in \mathbb{N}$ with $n \ge 3$, take a smallest regular $n$-sided polygon that encloses the unit circle). The polygon semi-lattices are also not well-founded, and thus we cannot obtain corollaries to Theorems 8 and 9 w.r.t. cyclic FBoxes.

## 3.3 Regular Languages

Given a finite alphabet $\Sigma$, the semi-lattice $\text{Reg}(\Sigma)$ consists of all regular languages over $\Sigma$, is partially ordered by set inclusion $\subseteq$, and its meet operation is set intersection $\cap$. It is not complete since regular languages are not closed under arbitrary intersections (only under finite ones). More specifically, $L = \cap\{\Sigma^* \setminus \{w\} \mid w \notin L\}$ for each language $L$, and thus for two symbols $a, b \in \Sigma$ the non-regular language $\{a^n b^n \mid n \in \mathbb{N}\}$ is an intersection of regular languages. Thus, convexity does not follow from Theorem 8.
In order to obtain a computable semi-lattice, we need to work with finite representations of regular languages. With regular expressions, binary intersections of regular languages can have exponential size even over a binary alphabet [25], i.e. the meet would not be computable in polynomial time. It is no alternative to instead use one-unambiguous/deterministic regular expressions since they cannot describe all regular languages and are not even closed under intersection, even though their inclusion problem is in polynomial time [19, 32, 48].

Using finite automata as representations is preferred, on the one hand since to obtain the meet/intersection of two regular languages we can compute the product of the respective finite automata in polynomial time [37]. On the other hand, a language inclusion $L_1 \subseteq L_2$ holds iff. the language equivalence $L_1 \cap L_2 = L_2$ holds, and thus it suffices to check if the product of both finite automata is equivalent to the second automaton. For deterministic automata this is possible in polynomial time [16, 31], but otherwise needs polynomial space [61].

The semi-lattice DFA($\Sigma$) consists of all deterministic finite automata over $\Sigma$, is partially ordered by automata inclusion $\preceq$ where $A \preceq B$ if $L(A) \subseteq L(B)$, and its meet operation is the product $\times$, which satisfies $L(A \times B) = L(A) \cap L(B)$. It is thus polynomial-time computable. Furthermore, FA($\Sigma$) comprises all finite automata and is polynomial-space computable. Since finite automata and deterministic ones have equal power in the sense that they both describe all regular languages, both semi-lattices can serve as representations of Reg($\Sigma$).

The hierarchical concrete domains $D_{\text{DFA}}(\Sigma)$ and $D_{\text{FA}}(\Sigma)$ are called the regular-language domains over $\Sigma$. Since single words are regular languages, precise string values are supported: we may write $(f = w)$ instead of $(f \preceq A)$ when $L(A) = \{w\}$. Further note that $\square$ is the automaton that accepts every string, $\perp$ accepts no string at all, and $\top$ is an artificial greatest element.

**Example 22.** Let $\Sigma$ be an alphabet containing all Latin letters, e.g. The Unicode Standard. We use a feature `hasTitle` to represent the title string of a research paper. Further take a DFA $A$ such that $L(A) = \Sigma^* \circ \{\text{description logic}\} \circ \Sigma^*$. With that, the CI `ScientificArticle` $\sqcap$ (`hasTitle \preceq A`) $\sqsubseteq$ `DLPaper` expresses that the concept of all DL papers subsumes the concept of all scientific articles with a title containing “description logic” as substring.

Even without an FBox, the regular-language domains $D_{\text{DFA}}(\Sigma)$ and $D_{\text{FA}}(\Sigma)$ are in general not P-admissible. In a nutshell, meets need not be non-duplicating, and thus accumulating all upper bounds of the same feature could yield an exponentially large automaton. More specifically, if a constraint set $\Gamma$ contains several constraints $f \le A$ for the same feature $f$, then computing the value $v_{\Gamma, \mathcal{F}}(f)$ boils down to computing the intersection of all these automata $A$. Since emptiness of intersections of finite automata is PSpace-hard [43] and graph reachability is NL-complete [35], $v_{\Gamma, \mathcal{F}}(f)$ cannot be computed in polynomial time, unless $P = PSpace$. We obtain, however, the following corollary to Proposition 11.

**Corollary 23.** W.r.t. each acyclic FBox $\mathcal{F}$ in which all occurring operations are polynomial-time computable, the regular-language domain $D_{\text{DFA}}(\Sigma)$ has exponential-time computable canonical valuations and is EXP-admissible.
The DFA operations corresponding to the language operations union $\cup$, intersection $\cap$, and complement $\bar{\phantom{}}$ are polynomial-time computable. $D_{\text{DFA}}(\Sigma)$ is thus EXP-admissible w.r.t. each acyclic FBox involving these operations only. In contrast, concatenation $\circ$, Kleene-star $^*$, mirror/reversal $\bar{\phantom{}}$, left-quotients $\backslash$, and right-quotients $/$ on DFAs are exponential-time computable but not polynomial-time computable [65]. However on FAs, all operations but complement are polynomial-time computable, and mirror/reversal is even non-duplicating. $D_{\text{FA}}(\Sigma)$ is EXP Space-admissible w.r.t. acyclic FBoxes using these polynomial-time operations.

It is worth mentioning that, if we have at most one inclusion (i.e. constraint or FI) per feature, then in the procedure in the proof of Theorem 9 neither the automata product operation nor the automata inclusion relation needs to be used, and so we have the following corollary.

**Corollary 24.** Let $\mathcal{F}$ be an acyclic, non-duplicating FBox in which all occurring operations are polynomial-time computable. Further let $\Gamma$ be a constraint set. If $\mathcal{F} \cup \Gamma$ contains, for each feature $f$, at most one inclusion with $f$ on the left, then the canonical valuation of $\Gamma$ w.r.t. $\mathcal{F}$ can be computed in polynomial time.

*Example 25.* Assume the features givenName, familyName, and name are used to represent persons' names. Then for instance, the concept Male $\sqcap$ (givenName $\preceq$ Name) where $L(\mathfrak{A}) = \{\mathfrak{F}\} \circ \Sigma^*$ describes all males whose given name starts with 'F'.

Moreover, the FI name $\preceq$ givenName $\circ \{\phantom{)}\}$ $\circ$ familyName allows to infer a regular language value of name when values of givenName and familyName are available (i.e. both are not $\top$). If the latter two are precise values (languages consisting of a single word), then also name gets a precise value through the FI. Note that ‘_’ stands for a white space. The FI shortName $\preceq$ initial(givenName) $\circ$ \{\_\} $\circ$ familyName generates a shortened form of a name that only contains the initial of the given name followed by a dot, where the function initial is defined by $L(initial(\mathfrak{A})) := \{s \mid s \in \Sigma \text{ and there is } w \in \Sigma^* \text{ such that } s \circ w \in L(\mathfrak{A})\}$.

The semi-lattices Reg($\Sigma$), DFA($\Sigma$), and FA($\Sigma$) are not well-founded since, already over the unary alphabet $\{a\}$, the regular languages $L_i := \{a^j \mid i \le j\}$ where $i \in \mathbb{N}$ form an infinite descending chain $L_0 \supset L_1 \supset L_2 \supset \dots$. These semi-lattices are also not complete (see above). W.r.t. cyclic FBoxes, we can thus not conclude convexity by Theorems 8 and 9.

For a restricted class of FBoxes, however, we obtain systems of language inclusions known to be solvable in exponential time [10]. An $n$-ary operation $H$ on DFA($\Sigma$) is left-linear if $H(\mathfrak{X}_1, \dots, \mathfrak{X}_n) = \mathfrak{X}_1 \circ \mathfrak{A}_1 \cup \dots \cup \mathfrak{X}_n \circ \mathfrak{A}_n \cup \mathfrak{B}$ and right-linear if $H(\mathfrak{X}_1, \dots, \mathfrak{X}_n) = \mathfrak{A}_1 \circ \mathfrak{X}_1 \cup \dots \cup \mathfrak{A}_n \circ \mathfrak{X}_n \cup \mathfrak{B}$, where $\mathfrak{A}_1, \dots, \mathfrak{A}_n, \mathfrak{B}$ are DFAs. An FBox $\mathcal{F}$ is linear if the operations in its FIs are either all left-linear or all right-linear.

**Proposition 26.** The regular-language domain $D_{\text{DFA}}(\Sigma)$ has exponential-time computable canonical valuations and is EXP-admissible w.r.t. each linear FBox.

If precise values (single words) are sufficient for the application, we could also use the semi-lattice $(\Sigma^* \cup \{\bot, \top\}, \le, \wedge)$ where $\le$ is the smallest partial order such
<figure><img src="image_18.png" /><figcaption>Fig. 1. Three graphs representing chemical compounds</figcaption></figure>

that $\perp < w < \top$ for each $w \in \Sigma^*$. The meet operation $\wedge$ thus satisfies $\top \wedge w = w$, $w \wedge w = w$, and $w \wedge \perp = \perp$ for each $w \in \Sigma^* \cup \{\perp, \top\}$, and $w_1 \wedge w_2 = \perp$ whenever $w_1, w_2 \in \Sigma^*$ with $w_1 \neq w_2$. This semi-lattice is complete and, by Theorem 8, its hierarchical concrete domain is convex w.r.t. every FBox. Since during the computation of a canonical valuation each feature value can be refined at most two times (from $\top$ to some $w$, and then possibly to $\perp$), this concrete domain is P-admissible w.r.t. each FBox in which all operations are polynomial-time computable. The disadvantage is, however, that string search like in Example 22 is not possible anymore. On the other hand, this suggests that in $D_{\mathbf{DFA}}(\Sigma)$ and $D_{\mathbf{FA}}(\Sigma)$ everything involving only precise values is possible in polynomial time.

## 3.4 Graphs

All finite, labeled graphs constitute a semi-lattice **Graph**, where the partial order $\leq$ is defined by $G \leq H$ if there is a homomorphism from $H$ to $G$. It is well-known that $\leq$ is NP-complete [21], but in P for acyclic graphs [22]. The meet of two graphs is their disjoint union, thus a non-duplicating operation, and the greatest element in this semi-lattice is the empty graph. Obviously, **Graph** is neither complete nor well-founded, and so we cannot apply Theorems 8 and 9. It thus remains unclear whether the *graph domain* $D_{\mathbf{Graph}}$ is convex w.r.t. cyclic FBoxes.

**Corollary 27.** The graph domain $D_{\mathbf{Graph}}$ has computable canonical valuations w.r.t. acyclic FBoxes. Moreover, it is NP-admissible w.r.t. every acyclic, non-duplicating FBox in which all operations are polynomial-time computable, and it is EXP-admissible w.r.t. every acyclic FBox in which all operations are polynomial-time computable.

*Example 28.* Structural formulas of molecules can be represented as labeled graphs. Each node is labeled with the atom it represents, and the edges are labeled with the binding type (e.g. single bond, double bond, etc.). Figure 1 shows three exemplary graphs. Graph (c) represents L-leucine, and we can integrate it into a KB with the statement $\mathbf{L-Leucine} \equiv (\mathbf{hasMolecularStructure} \leq \mathcal{G}_{\mathbf{L-leucine}})$. Moreover, the statement $\mathbf{AminoAcid} \equiv (\mathbf{hasMolecularStructure} \leq \mathcal{G}_{\text{carboxylic acid group}}) \sqcup (\mathbf{hasMolecularStructure} \leq \mathcal{G}_{\text{amino group}})$ expresses that amino acids are organic compounds that contain both amino and carboxylic acid functional groups. If $K$ is the KB consisting of the aforementioned statements, then $K \models \mathbf{L-Leucine} \sqsubseteq \mathbf{AminoAcid}$ since $\mathcal{G}_{\mathbf{L-leucine}} \leq \mathcal{G}_{\text{carboxylic acid group}} \wedge \mathcal{G}_{\text{amino group}}$.
# 4 Reasoning in $\mathcal{EL}^{++}$ with Hierarchical Concrete Domains

Like other convex concrete domains, a hierarchical concrete domain $D_L$ can be integrated into $\mathcal{EL}^{++}$ but, in addition to Sect. 2, every $\mathcal{EL}^{++}[D_L]$ KB may contain finitely many FIs. Of course, a model of such a KB must also satisfy all FIs in it. In order to guarantee that reasoning is decidable, a restriction on the interplay of RIs and range inclusions must be fulfilled by every $\mathcal{EL}^{++}[D]$ KB [5], see Condition 1 below. To this end, we define the range set of a role $r$ in $K$ by $\text{Range}(r, K) := \{C \mid \text{there is a role } s \text{ s.t. } \mathcal{R} \models r \sqsubseteq s \text{ and } \text{Ran}(s) \sqsubseteq C \in K\}$, where $\mathcal{R}$ is the subset of all RIs in $K$. All such range sets can be computed in polynomial time by first transforming each RI $r_1 \circ \cdots \circ r_n \sqsubseteq s$ into a context-free grammar rule $s \to r_1 \dots r_n$ (see Lemma IV in [9] for details) and then deciding the word problem for this grammar (e.g. with the CYK algorithm [23, 39, 64]).

**Definition 29.** Consider a bounded semi-lattice L. An $\mathcal{EL}^{++}[D_L]$ knowledge base (KB) $K$ is a finite set of CIs, RIs, range inclusions, and FIs such that

1. $\text{Range}(s, K) \subseteq \text{Range}(r_n, K)$ for every RI $r_1 \circ \cdots \circ r_n \sqsubseteq s$ in $K$ with $n \ge 2$,

2. and the hierarchical concrete domain $D_L$ is convex w.r.t. all FIs in $K$.

For a complexity class C we say that $D_L$ is C-admissible w.r.t. $K$ if $D_L$ is C-admissible w.r.t. the FBox consisting of all FIs in $K$.

For Condition 1 range inclusions on $s$ must not imply further concept memberships than already implied by the range inclusions on $r_n$; otherwise emptiness of intersections of two context-free grammars could be reduced to subsumption [5].

Reasoning in $\mathcal{EL}^{++}[D]$ can be done by means of a rule-based calculus [4, 5, 40, 42], and a hierarchical concrete domain $D_L$ can be seamlessly integrated into this calculus. Compared to the primal calculus [4, 5], it is only necessary to take the FIs into account. For integration into the improved calculus [40, 42] we only need to add the following two rules responsible for interaction between concrete and logical reasoning (where $\mathcal{F}$ consists of all FIs in the KB), see [46] for details.

$$ R_D: \frac{C \sqsubseteq (f_1 \le p_1) \cdots C \sqsubseteq (f_m \le p_m)}{C \sqsubseteq (g \le q)} : D_L, \mathcal{F} \models \prod_{i=1}^{m} (f_i \le p_i) \sqsubseteq (g \le q) $$

$$ R_{D,\perp}: \frac{C \sqsubseteq (f_1 \le p_1) \cdots C \sqsubseteq (f_m \le p_m)}{C \sqsubseteq \perp} : \prod_{i=1}^{m} (f_i \le p_i) \text{ unsatisfiable in } D_L, \mathcal{F} $$

However, we restrict attention to nominal-safe KBs, i.e. nominals $\{i\}$ must not occur in conjunctions and each right-hand side of a concept or range inclusion must not be a single nominal $\{i\}$. Full support for nominals in $\mathcal{EL}^{++}[D]$ is technically quite involved and makes reasoning more expensive: the degree of the polynomial describing the worst-case reasoning time would then be larger by 1 [41]. We conjecture the same for $\mathcal{EL}^{++}[D_L]$ KBs that are not nominal-safe.

Range inclusions are not natively supported by the rule-based calculus, but they must rather be eliminated [5]. This transformation was originally described for KBs in normal form only, but can now be done without prior transformation to normal form, see [46] for details.
**Theorem 30.** Let $\mathbf{L}$ be a bounded semi-lattice. For all nominal-safe $\mathcal{EL}^{++}[\mathcal{D}_{\mathbf{L}}]$ KBs w.r.t. which the hierarchical concrete domain $\mathcal{D}_{\mathbf{L}}$ is P-admissible, the following reasoning tasks can be done in polynomial time: consistency, classification, subsumption checking, instance checking, and concept satisfiability.

In the proof of the above result, we build a canonical model of the KB iff. it is consistent. Now with the hierarchical concrete domains we can use the canonical valuations for this. The benefit is that the canonical model is universal w.r.t. all nominal-safe assertions $\{i\} \sqsubseteq C$, before it was only universal w.r.t. such assertions without concrete constraints. Our canonical models are thus appropriate for computing optimal repairs [8, 9, 44, 45] of KBs involving concrete domains.

We can also use NP- or EXP-admissible concrete domains in $\mathcal{EL}^{++}$. Reasoning works in the very same way, i.e. the logical reasoning can still be done in polynomial time, but the concrete reasoning is more expensive.

**Theorem 31.** Fix a bounded semi-lattice $\mathbf{L}$. For all nominal-safe $\mathcal{EL}^{++}[\mathcal{D}_{\mathbf{L}}]$ KBs w.r.t. which the hierarchical concrete domain $\mathcal{D}_{\mathbf{L}}$ is NP-admissible, the following reasoning problems are in NP: consistency, concept satisfiability, subsumption checking, and instance checking. They are in EXP if $\mathcal{D}_{\mathbf{L}}$ is EXP-admissible. In both cases, the classification can be computed in exponential time.

# 5 Future Prospects

An interesting question for future research is whether non-local feature inclusions $f \le H(R_1 \circ g_1, \dots, R_n \circ g_n)$ would lead to undecidability or could be reasoned with, where the $R_i$ are role chains. The operator must then be defined for lists of values, like in the non-local feature inclusion $\text{combinedWealth} \subseteq \sum (\text{hasAccount} \circ \text{balance}) + \sum (\text{holdsAsset} \circ \text{value})$ over the interval domain, which computes the aggregated wealth of a person or company. At first sight, it seems that the undecidability proof for $\mathcal{EL}(\mathcal{D}_{Q^2, \text{aff}})$ [13] cannot be adapted to this setting. (Mind the braces: $(\mathcal{D})$ instead of $[\mathcal{D}]$ allows for role chains in front of features.) The computation of canonical valuations must then take into account the graph structure induced by the role assertions entailed by the knowledge base.

In general, it is unclear whether a hierarchical concrete domain is admissible w.r.t. cyclic FBoxes. According to our results for interval domains and regular-language domains, admissibility can be ensured by approaches to solving systems of equations or inequations involving elements of the underlying semi-lattice. This is still open for the polygon domains and the graph domains.

Since hierarchical concrete domains are convex by design, they are also appropriate for other Horn logics and existential rules—extending the chase procedure with support for them would be practically relevant.

**Acknowledgments.** This work has been supported by Deutsche Forschungsgemeinschaft (DFG) in Projects 389792660 (CPEC) and 558917076 as well as by the Saxon State Ministry for Science, Culture, and Tourism (SMWK) by funding the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI).