Description Logics with Concrete Domains and General Concept Inclusions Revisited∗,† (Extended abstract) Franz Baader and Jakub Rydval Institute of Theoretical Computer Science, TU Dresden, Germany {franz.baader,jakub.rydval}@tu-dresden.de Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts [2]. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability [4,13]. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones con- sidered in the previous proofs may cause undecidability. We show by a reduction from the halting problem of two-register machines that concept satisfiability in the DL ALC(D) is undecidable if D is a structure with domain Q, Z, or N whose only predicate is the binary predicate +1 , which is interpreted as incrementation. Our proof is an an adaptation of the undecidability proof in [5] to the case where no zero test =0 is available. Even though both proofs use a functional role g to represent the transitions between configurations of a given two-register machine, the reduction also works if g is assumed to be an arbitrary role. One simply must use additional universal quantification to ensure that all the g-successors of an individual satisfy the same properties. It turns out that undecidability also holds if we use the ternary predicate + rather than the binary predicate +1 . Intuitively, with + we can easily test for equality with 0 since the number m is 0 iff m + m = m. Instead of incrementation by 1, we can then use addition of a fixed non-zero number. To regain decidability in the presence of GCIs and concrete domains, the notion of ω-admissible concrete domains was introduced in [14]. The main motivation for the definition of ω-admissible concrete domains was that they can capture qualitative calculi of time and space. In particular, it was shown in [14] that Allen’s interval logic [1] as well as the region connection calculus RCC8 [17] can be represented as ω-admissible concrete domains. To the best of our knowledge, no other ω-admissible concrete domains have been exhibited in the literature since then. The major contribution of the paper is to support locating new ω-admissible concrete domains by linking their definition to well-known notions from model ∗ Supported by DFG Graduiertenkolleg 1763 (QuantLA). † Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). theory. To this purpose, we first generalize the notion of ω-admissibility and the decidability result from concrete domains with only binary predicates as in [14] to concrete domains with predicates of arbitrary arity. We then introduce several model-theoretic properties of relational structures and show their con- nection to ω-admissibility. This allows us to formulate sufficient conditions for ω-admissibility using well-know notions from model theory, and thus to employ existing model-theoretic results to find new ω-admissible concrete domains. This is not the first model-theoretic description of a sufficient condition for decid- ability of reasoning in DLs with concrete domains in the presence of GCIs. The existence of homomorphism is definable (EHD) property was used in [10] to obtain decidability results for DLs with concrete domains. However, the way the concrete domain is integrated into the DL in [10] is different from the classical one employed by us and used in all other papers on DLs with concrete domains. In [10], constraints are always placed along a linear path stemming from a single individual, which is rather similar to the use of constraints in temporal logics [9,11]. In contrast, in the classical setting of DLs with concrete domains, one can compare feature values of siblings of an individual. The main result shown in this paper is that, under the natural assumption that concrete domains can express the binary equality predicate, there is a close connection between the patchwork property, an essential part of the ω- admissibility condition, and the amalgamation property. The latter plays a crucial role in Fraïssé’s theorem, which characterizes those classes of finite structures which arise as finite substructures of a countable homogeneous structure [12]. We use this connection to prove that the large class of finitely bounded homogeneous structures yields ω-admissible concrete domains. The facts that a great variety of homogeneous structures is known from the literature [16] and that finitely bounded homogeneous structures play an important rôle in the CSP community [8] support our claim that this work will turn out to be useful for locating new ω-admissible concrete domains. Finally, we discuss possible applications and limits for our approach. The algorithm from [15] for reasoning with ω-admissible concrete domains depends heavily on the finiteness of the signature. In principle, structures with an infinite signature satisfying similar conditions could also provide decidable extensions of ALC by concrete domains. However, there are examples of structures with infinite signatures satisfying most of our conditions that lead to undecidability if used as concrete domains. For instance, the structure with domain Z whose relations are of the form +k for every k ∈ Z is homogeneous, but ALC extended with this concrete domain is undecidable, even though satisfiability of finite conjunctions of constraints in this structure is decidable. Restricting the attention to structures over finite signatures has also other advantages. For a given finite set of binary predicates described by a finite set of bounds (which is the case for Allen and RCC8), it is actually decidable whether there exists a finitely bounded homogeneous structure which has precisely these as its relations [7]. We continue the discussion by showing how to reproduce some of the known proofs of ω-admissibility for specific concrete domains using our approach and how 2 to combine several concrete domains into one while preserving ω-admissibility. For the latter, we consider disjoint unions and also certain products which allow us to access finitely many concrete domains through coordinates of a single concrete domain living on the Cartesian product. Taking products instead of disjoint unions turns out to be necessary if one wants to describe several features of an individual at once in the presence of relational paths in concrete domain constructors. In our setting, ω-admissibility also remains preserved under expansions by finitely many constants, i.e., unary predicates of the form =d for domain elements d. Unfortunately, we cannot allow for infinitely many additional predicates of any sort since our algebraic tools are only applicable to finite signatures. Intuitively, the expansion of any structure by all domain elements is always homogeneous, but we lose all complexity-theoretic properties of the original structure, including finite boundedness. We finish the paper with an example of a structure that is ω-admissible but not finitely bounded. This shows that finitely bounded homogeneous structures do not exhaust the pool of ω-admissible concrete domains entirely. The paper containing these results was published at IJCAR 2020 [6]. References 1. Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM 26(11), 832–843 (1983) 2. Baader, F., Hanschke, P.: A schema for integrating concrete domains into concept languages. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI’91). pp. 452–457 (1991), long version available as [3] 3. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. Tech. Rep. RR-91-10, Deutsches Forschungszentrum für Künstliche Intel- ligenz (DFKI) (1991), available at https://lat.inf.tu-dresden.de/research/reports/ 1991/DFKI-RR-91-10.pdf 4. Baader, F., Hanschke, P.: Extensions of concept languages for a mechanical engineer- ing application. In: Proc. of the 16th German Workshop on Artificial Intelligence (GWAI’92). Lecture Notes in Computer Science, vol. 671, pp. 132–143. Springer- Verlag, Bonn (Germany) (1992) 5. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017) 6. Baader, F., Rydval, J.: Description logics with concrete domains and general concept inclusions revisited. In: Proc. of the 10th International Joint Conference on Automated Reasoning (IJCAR’20). Springer (2020), to appear 7. Bodirsky, M., Knäuer, S., Starke, F.: ASNP: A tame fragment of existential second- order logic. In: Anselmo, M., Vedova, G.D., Manea, F., Pauly, A. (eds.) Beyond the Horizon of Computability – 16th Conference on Computability in Europe, CiE 2020, Proceedings. Lecture Notes in Computer Science, vol. 12098, pp. 149–162. Springer (2020), preprint available at https://arxiv.org/abs/2001.08190.pdf 8. Bodirsky, M., Mottet, A.: Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 623–632. ACM/IEEE (2016) 3 9. Carapelle, C., Feng, S., Kartzow, A., Lohrey, M.: Satisfiability of ECTL∗ with local tree constraints. Theory Comput. Syst. 61(2), 689–720 (2017) 10. Carapelle, C., Turhan, A.Y.: Description logics reasoning wrt general TBoxes is decidable for concrete domains with the EHD-property. In: Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI’16). pp. 1440–1448. IOS Press (2016) 11. Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380–415 (2007) 12. Hodges, W.: A shorter model theory. Cambridge University Press (1997) 13. Lutz, C.: NExpTime-complete description logics with concrete domains. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001). pp. 45–60. No. 2083 in Lecture Notes in Artificial Intelligence, Springer-Verlag, Siena, Italy (2001) 14. Lutz, C., Milicic, M.: A tableau algorithm for description logics with concrete domains and general TBoxes. J. of Automated Reasoning 38(1–3), 227–259 (2007) 15. Lutz, C., Miličić, M.: A tableau algorithm for description logics with concrete domains and general TBoxes. Journal of Automated Reasoning 38(1-3), 227–259 (2007) 16. Macpherson, D.: A survey of homogeneous structures. Discrete Mathematics 311(15), 1599–1634 (2011) 17. Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’92). pp. 165–176. Morgan Kaufmann, Los Altos (1992) 4