On Mixed Semantics of Path Description Dependencies in FunDL Eva Feng1 , David Toman2 and Grant Weddell2 1 Department of Computer Science, Oxford University, Oxford, UK 2 Cheriton School of Computer Science, University of Waterloo, Waterloo, Canada Abstract The FunDL family of description logics replace roles with partial functions (features) and have a concept constructor called a path functional dependency (PFD) that can be used to capture a variety of equality-generating dependencies commonly part of conceptual designs as well as schemata of object-relational data sources. Recent work has considered replacing the PFD concept constructor with a more general path description dependency (PDD) in which inverse features are now allowed in characterizing feature path reachability in interpretations. This leads to a circumstance in which the value of a feature path for a given entity might be set-valued. This work has focused on cases in which feature path agreement is based exclusively on either a set intersection semantics or a non-empty set equality semantics. In this paper, we consider a mixed mode case for PDDs in which individual component feature paths can be assigned either of these options. Our main results are that this flexibility makes logical consequence undecidable in general, but that restricting an arbitrary mixed-mode for PDDs to conform to a mode-typing assignment on features re-obtains EXPTIME completeness for logical consequence. 1. Introduction Given a query over a conceptual ontological design for some domain, there are many circumstances in which reasoning about equality generating dependencies is essential in finding an efficient plan over available backend structured data sources such as relational databases, e.g., in resolving identity issues for entities in an underlying domain [1, 2], or in determining when explicit duplicate elimination in query plans is not required [3]. The FunDL family of description logics [4] has been developed largely for this purpose and therefore replace roles with partial functions (features) to better align with the ubiquitous notion of an attribute or column value and have a concept constructor called a path functional dependency (PFD) that can be used to capture a variety of equality-generating dependencies needed to resolve identity issues or are commonly part of schemata for structured data sources such as keys and (relational) functional dependencies. Recent work [5] has introduced a new dialect for FunDL called set-π’Ÿβ„’β„±π’Ÿβ„ that replaces the PFD concept constructor with a more general path description dependency (PDD) in which inverse features are now allowed in characterizing feature path reachability in interpretations, leading to a circumstance in which the value of a feature path for a given entity might be set-valued. This work has explored alternative semantics for PDDs, with a focus on cases in which feature path agreement is based exclusively on either a set intersection semantics or a non-empty set equality semantics, showing in both cases that allowing more general PDDs in place of PFDs does not change the complexity of logical consequence in any of the Boolean complete FunDL dialects, which remain EXPTIME complete in the worst case. The primary incentive for set-π’Ÿβ„’β„±π’Ÿβ„ stems from an outline of future work in [6] which recognized the need for plural entities in formally capturing JSON arrays, in particular, for the more general expressiveness of PDDs to capture how such array entities can be identified. The following inclusion dependencies are derived from a running example in [5] and illustrate this DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway $ eva.feng@cs.ox.ac.uk (E. Feng); david@uwaterloo.ca (D. Toman); gweddell@uwaterloo.ca (G. Weddell) Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings (where also CLIENT-FRIEND βŠ‘ CLIENT is assumed): CLIENT-FRIEND βŠ‘ CLIENT : firstname∩ , (phone-domβˆ’ .phone-ran.dialnum)∩ β†’ id ∩ CLIENT-FRIEND βŠ‘ CLIENT : (phone-domβˆ’ .phone-ran.dialnum)β‰ˆ β†’ id β‰ˆ Feature path reachability in the dependencies corresponds to four path descriptions (PDs): β€œfirstname”, β€œphone-domβˆ’ .phone-ran.dialnum” and β€œid ”. The first and last are PDs that also qualify as path functions (PFs) since their interpretations will be partial functions. The first dependency employs a PDD on its right-hand-side with set intersection semantics (indicated by the β€œβˆ©β€ superscript on PDs) to express a key or uniqueness condition for any client that is also a friend: among all clients, they will have a unique combination of a first name and the dial number of any of their phones. The second employs a PDD on its right-hand-side with non-empty set equality semantics (indicated by the β€œβ‰ˆβ€ superscript on PDs) to also express a key or uniqueness condition: among all clients with at least one phone, they have a unique set of dial numbers. Including both dependencies in a TBox has so far not been possible since this requires two distinct modes for the PD β€œphone-domβˆ’ .phone-ran.dialnum” in a PDD that appeal to both set intersection and non-empty set equality semantics for PD agreement, a circumstance now enabled by introducing annotated PDs in which a superscript arbitrates between a choice of semantics. Indeed, our primary concern in this paper is to study logical consequence for a new member of the FunDL family called set-π’Ÿβ„’β„±π’Ÿβ„ in which PDDs now allow annotated PDs as components. Our main results are that, unlike earlier work, this flexibility makes logical consequence undecidable in general, but that restricting an arbitrary mixed-mode for PDDs to conform to a mode-typing assignment on features re-obtains EXPTIME completeness for logical consequence for all members of the FunDL family. The remainder of the paper proceeds as follows. Section 2 introduces the relevant definitions, previous results and open questions regarding set-π’Ÿβ„’β„±π’Ÿβ„ that have motivated this paper. Section 3 shows the undecidability of entailment in set-π’Ÿβ„’β„±π’Ÿβ„ when a mixed semantics for path agreements is used. Section 3.1 shows how decidability can be regained by imposing a mild typing discipline on path agreements. Section 4 concludes the paper and outlines directions for further investigation. 2. Background and Definitions In this section we define the description logic set-π’Ÿβ„’β„±π’Ÿβ„. We start with defining primitive features and concepts, and how they are interpreted: Definition 1 (Vocabulary of set-π’Ÿβ„’β„±π’Ÿβ„). Let F and PC be sets of feature names and primitive concept names, respectively. Semantics is defined with respect to a structure ℐ = (△ℐ , ·ℐ ), where △ℐ is a domain of objects or entities and ·ℐ an interpretation function that fixes the interpretations of primitive concept names 𝐴 ∈ PC to be subsets of △ℐ and feature names 𝑓 ∈ F to be partial functions 𝑓 ℐ : △ℐ β†’ △ℐ . The primitive syntax and semantics is now extended to Path Descriptions and (eventually) to Concept Descriptions: Definition 2 (Path Descriptions in set-π’Ÿβ„’β„±π’Ÿβ„). A path description is defined by the grammar Pd ::= id | 𝑓. Pd | 𝑓 βˆ’ . Pd, for 𝑓 ∈ F, where 𝑓 βˆ’ is called the inverse of 𝑓 , with the stipulation that substrings of the form 𝑓.𝑓 βˆ’ and 𝑓 βˆ’ .𝑓 do not appear in any path description Pd. Let ℐ be an interpretation. Then the interpretations of ℐ ℐ path descriptions Pd are functions Pdℐ : 2β–³ β†’ 2β–³ over the powerset of △ℐ defined as follows, where 𝑆 βŠ† △ℐ : ⎧ ⎨ 𝑆 βŽͺ if Pd = β€œ id”, ℐ ℐ ℐ Pd (𝑆) = Pd1 ({𝑓 (π‘₯) | π‘₯ ∈ 𝑆}) if Pd = β€œπ‘“. Pd1”, ⎩ Pdℐ ({π‘₯ | 𝑓 ℐ (π‘₯) ∈ 𝑆}) if Pd = β€œπ‘“ βˆ’ . Pd ”. βŽͺ 1 1 Syntax Semantics: Defn of (Β·)ℐ 𝐢 ::= A Aℐ βŠ† △ℐ (primitive concept; A ∈ PC) ℐ ℐ | ¬𝐢 β–³ βˆ–πΆ (negation) ℐ ℐ | 𝐢1 βŠ“ 𝐢2 𝐢1 ∩ 𝐢2 (conjunction) | 𝐢1 βŠ” 𝐢2 𝐢1ℐ βˆͺ 𝐢2ℐ (disjunction) ℐ ℐ | βˆ€π‘“.𝐢 {π‘₯ | 𝑓 (π‘₯) ∈ 𝐢 } (value restriction) ℐ ℐ | βˆƒπ‘“ {π‘₯ | βˆƒπ‘¦ ∈ β–³ .𝑦 = 𝑓 (π‘₯)} (existential restriction) | βˆƒπ‘“ βˆ’ {π‘₯ | βˆƒπ‘¦ ∈ △ℐ .π‘₯ = 𝑓 ℐ (𝑦)} (existential restriction) ∼1 βˆΌπ‘˜ ∼ ℐ | 𝐢 : Pd1 , ..., Pdπ‘˜ β†’ Pd {π‘₯ | βˆ€ 𝑦 ∈ 𝐢 : (GD(Pd(π‘₯)) ∧ GD(Pd(𝑦)) ∧ (PDD) β‹€οΈ€π‘˜ 𝑖=1 Pd 𝑖 (π‘₯) βˆΌπ‘– Pd 𝑖 (𝑦)) β†’ Pd(π‘₯) ∼ Pd(𝑦)} Figure 1: Syntax and semantics of concept descriptions. Path Descriptions that do not contain inverse features are called path functions. Before we define concept descriptions of set-π’Ÿβ„’β„±π’Ÿβ„, we need the notion of path description agreement; this agreement is parameterized by how the results of applying a path description on a pair of objects are compared. We define and explore three possibilities here, the set equality, the non-empty set equality, and the set intersection based agreements. Formally: Definition 3 (Path Description Agreement). Let ℐ be an interpretation and π‘œ1 and π‘œ2 be two △ℐ elements. We say that π‘œ1 and π‘œ2 ∼-agree on Pd, written Pd(π‘œ1 ) ∼ Pd(π‘œ2 ), if β€’ Pdℐ ({π‘œ1 }) = Pdℐ ({π‘œ2 }) (set equality), when ∼ is β€œ=”, β€’ Pdℐ ({π‘œ1 }) = Pdℐ ({π‘œ2 }) ΜΈ= βˆ… (non-empty set equality), when ∼ is β€œβ‰ˆβ€, and β€’ Pdℐ ({π‘œ1 }) ∩ Pdℐ ({π‘œ2 }) ΜΈ= βˆ… (set intersection), when ∼ is β€œβˆ©β€. We use the Path Description Agreements (defined above) to define the logic set-π’Ÿβ„’β„±π’Ÿβ„ as follows: Definition 4 (Concept Descriptions, Subsumptions, and TBoxes in set-π’Ÿβ„’β„±π’Ÿβ„). A concept description 𝐢 is constructed from primitive concepts using Boolean concept constructors βŠ“, βŠ”, and Β¬, value restrictions on features βˆ€π‘“.𝐢, unqualified existential restrictions on features and inverse features βˆƒπ‘“ and βˆƒπ‘“ βˆ’ , and the path description dependency (PDD) of the form βˆΌπ‘˜ 𝐢 : Pd∼ ∼ 1 , ..., Pdπ‘˜ β†’ Pd . 1 The semantics of all the derived concept descriptions 𝐢 is defined in Figure 1 where GD(Pd(𝑧)) is β€’ true (unconstrained), when ∼ is β€œ=”, and β€’ Pdℐ (𝑧) ΜΈ= βˆ… (non-empty), when ∼ is β€œβ‰ˆβ€ or β€œβˆ©β€. A subsumption is an expression of the form 𝐢1 βŠ‘ 𝐢2 , where the 𝐢𝑖 are concepts, and where PDDs occur only in 𝐢2 but not within the scope of negation.1 A terminology (TBox) 𝒯 consists of a finite set of subsumptions, and a posed question 𝒬 is a single subsumption. An interpretation ℐ satisfies a subsumption 𝐢1 βŠ‘ 𝐢2 if 𝐢1ℐ βŠ† 𝐢2ℐ and is a model of 𝒯 , written ℐ |= 𝒯 , if it satisfies all subsumptions in 𝒯 . Given a terminology 𝒯 and posed question 𝒬, the logical consequence problem asks if 𝒬 is satisfied in all models of 𝒯 , written 𝒯 |= 𝒬. β–‘ Observe that the proposed logic lacks qualified existential restrictions. Indeed, entailment for partial-π’Ÿβ„’β„±π’Ÿβ„ with qualified existential restrictions over inverse features was shown in [9] to be 1 Violating this latter condition leads immediately to undecidability [7, 8]. undecidable, which will therefore also be the case with set-π’Ÿβ„’β„±π’Ÿβ„. However, for a feature 𝑓 , one can substitute the subsumption 𝐴 βŠ‘ βˆƒπ‘“.𝐡 with two subsumptions 𝐴 βŠ‘ βˆƒπ‘“ and βˆ€π‘“.𝐡 βŠ‘ 𝐴, which completely characterizes the behaviour of the qualified existential restriction. Note that an analogous substitution for 𝐴 βŠ‘ βˆƒπ‘“ βˆ’ .𝐡, namely 𝐴 βŠ‘ βˆƒπ‘“ βˆ’ and βˆ€π‘“.𝐴 βŠ‘ 𝐡, will only partially capture the behaviour of an existential restriction for inverse features, a limitation needed to regain decidability of entailment. In the remainder of the paper, we allow using βˆƒPd.𝐢 to serve as a shorthand for applying the above substitutions systematically on Pd by splitting the Pd to individual features and introducing auxiliary primitive concepts. On Guards in PDDs One may wonder if the additional guards GD(Pd(π‘₯)) and GD(Pd(𝑦)) imposed on the consequent path descriptions in a PDD are needed with the {∩, β‰ˆ} adornments. Consider the following pair of subsumptions, for each 0 < 𝑖 ≀ π‘˜, π‘˜ β‰₯ 2: 𝐴 βŠ‘ 𝐴 : (𝑖𝑑)∩ β†’ (𝑓 βˆ’ .𝑔𝑖 )∩ and βˆ€π‘”π‘– .⊀ βŠ‘ 𝐡𝑖 . It is easy to see that these pairs of subsumptions entail 𝐴 βŠ‘ βˆƒπ‘“ βˆ’ .𝐡𝑖 . In the absence of the guards in the PDD semantics one can add subsumptions 𝐡𝑖 βŠ“ 𝐡𝑗 βŠ‘ βŠ₯ for 𝑖 ΜΈ= 𝑗 that will force every 𝐴 individual to have a distinct 𝑓 predecessor for each 𝐡𝑖 . This leads immediately to undecidability without guards since it allows one to simulate qualified existential restrictions over inverse features [9]. Note that including the guards with a PDD ensures that a right-hand-side will not β€œforce” path existence. Past Work The above definition of PDDs can be specialized in several ways, some of which have been considered in the past. 1. In [5] we have considered the set intersection semantics for set-π’Ÿβ„’β„±π’Ÿβ„, a semantics in which the ∼ agreements in all PDDs were defined as β€œβˆ©β€ (non-empty set intersection). However, we have required that all the path descriptions involved in any PDD must exist before the PDD applies, i.e., the semantics was defined as (𝐢 : Pd1 , ..., Pdπ‘˜ β†’ Pd)ℐ = {π‘₯ | βˆ€ 𝑦 ∈ 𝐢 ℐ : Pdℐ ({π‘₯}) ΜΈ= βˆ… ∧ Pdℐ ({𝑦}) ΜΈ= βˆ… ∧ ( π‘˜π‘–=1 Pdℐ𝑖 ({π‘₯}) ∩ Pdℐ𝑖 ({𝑦}) ΜΈ= βˆ…) β†’ Pdℐ ({π‘₯}) ∩ Pdℐ ({𝑦}) ΜΈ= βˆ…}. β‹€οΈ€ Under the set intersection semantics, the logical consequence problem for partial-π’Ÿβ„’β„±π’Ÿβ„, and consequently its derivative set-π’Ÿβ„’β„±π’Ÿβ„, is EXPTIME-complete. We have shown that the problem is in EXPTIME by constructing a two-tree model and then reducing to the satisfiability of an Ackermann formula encoding the logical consequence problem. Completeness then follows from EXPTIME-hardness of the implication problem for the {D1 βŠ“ D2 , βˆ€π‘“.D1 } and {⊀, ⊀ : Pf 1 , Pf 2 β†’ Pf} fragments of FunDL [10]. 2. Also in [5], we have considered the set equality semantics for set-π’Ÿβ„’β„±π’Ÿβ„, a semantics in which the ∼ agreements in all PDDs were defined as β€œ=”, (𝐢 : Pd1 , ..., Pdπ‘˜ β†’ Pd)ℐ = {π‘₯ | βˆ€ 𝑦 ∈ 𝐢 ℐ : ( π‘˜π‘–=1 Pdℐ𝑖 ({π‘₯}) = Pdℐ𝑖 ({𝑦})) β‹€οΈ€ β†’ Pdℐ ({π‘₯}) = Pdℐ ({𝑦})}. We have shown that under the set equality semantics, the ability to assert equality of non-existent paths in a PDD’s precondition allows us to create nominal-like concepts which leads immediately to undecidability. Set-Intersection vs. Set-Equality Empty Set Type Complexity Set-Intersection No (by definition) – EXPTIME-complete [5] Set-Equality Yes – Undecidable [5] Set-Equality No – EXPTIME-complete (new) Both No for Set-Equality Mixed Undecidable (new) Both No for Set-Equality Typed EXPTIME-complete (new) Figure 2: Complexity of set-π’Ÿβ„’β„±π’Ÿβ„ Based on Various Semantics 3. To regain decidability under the set equality semantics, we preclude the equality of empty sets by a non-empty set equality semantics defined as follows, (𝐢 : Pd1 , ..., Pdπ‘˜ β†’ Pd)ℐ = {π‘₯ | βˆ€ 𝑦 ∈ 𝐢 ℐ : Pdℐ ({π‘₯}) ΜΈ= βˆ… ∧ Pdℐ ({𝑦}) ΜΈ= βˆ… ∧ ( π‘˜π‘–=1 Pdℐ𝑖 ({π‘₯}) = Pdℐ𝑖 ({𝑦}) ΜΈ= βˆ…) β†’ Pdℐ ({π‘₯}) = Pdℐ ({𝑦})}. β‹€οΈ€ which brings the complexity back to EXPTIME-complete. The proof for non-empty set equality semantics is essentially the same as the one for set intersection semantics [5]. In this paper we consider the remaining possibilities (some of which were posed as open problems). 4. We have conjectured that mixing the set intersection and non-empty set equality semantics, both of which are decidable, could lead to undecidability. In this paper, we show that allowing combinations of the EXPTIME-complete semantics in the PDs leads to undecidability by reduction of the unconstrained tiling problem. Note that for path functions there is no difference between the set intersection agreements and non-empty set agreements; hence we omit the type of the agreement in the remaining constructions for path functions. 5. Curiously, we can restrict arbitrary mixed semantics by virtue of fixing the type of semantics for each feature 𝑓 and inverse feature 𝑓 βˆ’ , which generalizes to PDs. In Section 3.1, we show that adopting such typed mixed semantics allows us to regain EXPTIME-completeness. We summarize the complexity results for set-π’Ÿβ„’β„±π’Ÿβ„ based on various combinations of set intersection and set equality-based semantics in Figure 2. 3. Undecidability of Mixed PDDs In this section, we show that allowing both non-empty set equality and set intersection semantics simultaneously in the PDDs leads to undecidability by reduction of a tiling problem that allows one to simulate runs of a Turing Machine on an empty input tape, a problem that is known to be undecidable [11]. An instance π‘ˆ of the tiling problem is a triple (𝑇, 𝐻, 𝑉 ), consisting of a set 𝑇 of tile types and 𝐻, 𝑉 βŠ† 𝑇 Γ— 𝑇 two binary relations. A solution to π‘ˆ is a function 𝑑 : N Γ— N β†’ 𝑇 such that, for 𝑖 < 𝑗, we have (𝑑(𝑖, 𝑗), 𝑑(𝑖 + 1, 𝑗)) ∈ 𝐻 and (𝑑(𝑖, 𝑗), 𝑑(𝑖, 𝑗 + 1)) ∈ 𝑉 . This tiling solution covers an infinite triangle of successive longer and longer tapes (instantaneous descriptions) and this way simulates a run of a given Turing Machine2 . We construct a terminology along with a posed question, denoted 𝒯 (𝑇, 𝐻, 𝑉 ), for a given tiling problem π‘ˆ , in the following steps. Theorem 5. An instance (𝑇, 𝐻, 𝑉 ) of the unconstrained tiling problem admits a solution if and only if 𝒯 (𝑇, 𝐻, 𝑉 ) ΜΈ|= A βŠ‘ 𝐷 : 𝑓 β†’ id for a 𝒯 (𝑇, 𝐻, 𝑉 ) TBox corresponding to the instance (𝑇, 𝐻, 𝑉 ). Proof (sketch): Given a tiling problem (𝑇, 𝐻, 𝑉 ) we construct a TBox 𝒯 (𝑇, 𝐻, 𝑉 ) that utilizes pairwise disjoint primitive concepts A, B, and C to serve as grid points and an auxiliary diagonal primitive concept D. We assume that the features 𝑓 , 𝑔, β„Ž, and π‘˜ are total, and the inverse 𝑓 βˆ’ is total on A, B, C, and D. These are captured by 𝒯 (𝑇, 𝐻, 𝑉 ) subsumptions 2 The reduction is essentially the same as for the classical tiling of a full quadrant, but starts with an empty tape. ↑ β†– 𝑓 𝑓 A Dβ†– ↑ ↑ 𝑓 𝑓 𝑓 A 𝑔 β†’ ← 𝑔 B Dβ†– 𝑔 β†’ ↑ ↑ ↑ 𝑓 𝑓 𝑓 𝑓 A 𝑔 β†’ ← 𝑔 B β„Ž β†’ ← β„Ž C Dβ†– β„Ž β†’ ↑ ↑ ↑ ↑ 𝑓 𝑓 𝑓 𝑓 𝑓 A 𝑔 β†’ ← 𝑔 B β„Ž β†’ ← β„Ž C π‘˜ β†’ ← π‘˜ A Dβ†– π‘˜ β†’ ↑ ↑ ↑ ↑ ↑ 𝑓 𝑓 𝑓 𝑓 𝑓 𝑓 A 𝑔 β†’ ← 𝑔 B β„Ž β†’ ← β„Ž C π‘˜ β†’ ← π‘˜ A 𝑔 β†’ ← 𝑔 B D 𝑔 β†’ Figure 3: Construction of a Grid for Tiling. ⊀ βŠ‘ βˆƒπ‘“ βŠ“ βˆƒπ‘” βŠ“ βˆƒβ„Ž βŠ“ βˆƒπ‘˜ A βŠ” B βŠ” C βŠ” D βŠ‘ βˆƒπ‘“ βˆ’ ; and (1) A βŠ“ B βŠ‘ βŠ₯, A βŠ“ C βŠ‘ βŠ₯, A βŠ“ D βŠ‘ βŠ₯, B βŠ“ C βŠ‘ βŠ₯, B βŠ“ D βŠ‘ βŠ₯, C βŠ“ D βŠ‘ βŠ₯. To show the non-entailment we need to construct a counterexample to the posed question, A βŠ‘ 𝐷 : 𝑓 β†’ id that satisfies all subsumptions in 𝒯 (𝑇, 𝐻, 𝑉 ). We construct the TBox 𝒯 (𝑇, 𝐻, 𝑉 ) for an instance of a tiling problem (𝑇, 𝐻, 𝑉 ) in such a way that the counterexample will correspond to a solution to this tiling problem. In what follows we list all the subsumptions needed in 𝒯 (𝑇, 𝐻, 𝑉 ) to achieve this goal. The subsumption A βŠ‘ D : 𝑓 β†’ (𝑓 βˆ’ .𝑔)∩ (and B βŠ‘ D : 𝑓 β†’ (𝑓 βˆ’ .β„Ž)∩ , C βŠ‘ D : 𝑓 β†’ (𝑓 βˆ’ .π‘˜)∩ ), (2) stating that A and D that agree on 𝑓 must ∩-agree on 𝑓 βˆ’ .𝑔 (and that B and D that agree on 𝑓 must ∩-agree on 𝑓 βˆ’ .β„Ž and C and D that agree on 𝑓 must ∩-agree on 𝑓 βˆ’ .π‘˜, respectively), the subsumption A βŠ‘ D : (𝑓 βˆ’ .𝑔)β‰ˆ β†’ id (and B βŠ‘ D : (𝑓 βˆ’ .β„Ž)β‰ˆ β†’ id , C βŠ‘ D : (𝑓 βˆ’ .π‘˜)β‰ˆ β†’ id ), (3) stating that A and D above must β‰ˆ-disagree on those paths, in order not to equate an A object with an D object (and similarly for B and D, and C and D, respectively), together with subsumption extending the A (and similarly B and C, respectively) class memberships along 𝑓 predecessors βˆ€π‘“.A βŠ‘ A (and βˆ€π‘“.B βŠ‘ B, βˆ€π‘“.C βŠ‘ C) (4) and subsumptions ensuring those predecessors–with respect to a particular class membership–are unique, D βŠ‘ D : 𝑓 β†’ id , (5) A βŠ‘ A : 𝑓 β†’ id , (and B βŠ‘ B : 𝑓 β†’ id , C βŠ‘ C : 𝑓 β†’ id ), force this counterexample to look like the first three top rows in Figure 3 (with the exception of class membership of the final two objects in the third row). Note that the A object’s 𝑓 predecessors are also A objects due to (4). Moreover the A predecessors are unique due to (5). Hence the D object at the end of row 2 must have at least two incoming 𝑓 features to satisfy (2) and (3) simultaneously while not violating the disjointness of A and D in (1). The same holds for the right-most B and C objects used in the construction of the subsequent rows. The now existing horizontal right neighbours of the object A in the 3rd row are assigned concept membership using the following subsumptions: A βŠ‘ Β¬B : 𝑔 β†’ 𝑖𝑑 (and B βŠ‘ Β¬C : β„Ž β†’ 𝑖𝑑, C βŠ‘ Β¬A : π‘˜ β†’ 𝑖𝑑); (6) B βŠ‘ Β¬D : 𝑓 β†’ 𝑖𝑑 (and C βŠ‘ Β¬D : 𝑓 β†’ 𝑖𝑑, A βŠ‘ Β¬D : 𝑓 β†’ 𝑖𝑑), i.e., the right (𝑔.𝑔 βˆ’ ) neighbour of A must be B, etc. In particular, the object D at the end of row 2 must have exactly two incoming 𝑓 features, one from an B and second from a D objects. This completes the construction of the top three rows in Figure 3. To replicate this process for row 4 in Figure 3 we use the second subsumptions in (2), (3), (4), (5), (6), and (7). To complete the left part(s) of the grid–the squares below A, B, and C objects we use the following subsumptions: A βŠ‘ B : 𝑓.𝑔 β†’ 𝑔 (and B βŠ‘ C : 𝑓.β„Ž β†’ β„Ž, C βŠ‘ A : 𝑓.π‘˜ β†’ π‘˜); (7) Analogously, the 3rd subsumptions in (2), (3), (4), (5), (6), and (7) will construct row 5. The end of row 5 presents a situation that is a copy of the pattern in row 2 and the hence the construction starts repeating itself indefinitely and extends to an infinite triangle by simply repeating the above steps. To finish the construction we need to assign tiles to all grid points, A βŠ” B βŠ” C βŠ‘ βŠ”π‘‘π‘– βˆˆπ‘‡ T𝑖 , (8) and enforce the horizontal, T𝑖 βŠ“ A βŠ‘ (T𝑗 βŠ“ B) : 𝑔 β†’ id , T𝑖 βŠ“ B βŠ‘ (T𝑗 βŠ“ C) : β„Ž β†’ id , (9) T𝑖 βŠ“ C βŠ‘ (T𝑗 βŠ“ A) : π‘˜ β†’ id , βˆ€(𝑑𝑖 , 𝑑𝑗 ) ∈ / 𝐻, and vertical tiling rules, βˆ€π‘“.(T𝑖 βŠ“ A) βŠ“ T𝑗 βŠ‘ βŠ₯, βˆ€π‘“.(T𝑖 βŠ“ B) βŠ“ T𝑗 βŠ‘ βŠ₯, (10) βˆ€π‘“.(T𝑖 βŠ“ C) βŠ“ T𝑗 βŠ‘ βŠ₯, βˆ€(𝑑𝑖 , 𝑑𝑗 ) ∈ / 𝑉. In summary, a TBox 𝒯 (𝑇, 𝐻, 𝑉 ) containing all the subsumptions (1), (2), (3), (4), (5), (6), (7), (8), (9), and (10) does not entail the posed question if and only if a tiling exists. The existence of a non-terminating computation of a given Turing machine starting with an empty tape can now be witnessed by the existence of a tiling using the standard encoding of instantaneous descriptions of the TM’s computations as rows in the tiling overlayed over Figure 3; the computation steps then correspond to the consecutive rows of tiles. Note that tiling of the infinite triangle is sufficient as the TM’s head can move at most one cell to the right for every step of the computation. β–‘ Alternatively, to tile a full quadrant, we can use the vertical 𝑓 -antichains as columns (as above) and diagonals starting from the left-most A-labelled column as rows. This needs a slight adjustment to the horizontal tiling subsumptions (9) as follows: βˆ€π‘“.(T𝑖 βŠ“ A) βŠ‘ (T𝑗 βŠ“ B) : 𝑔 β†’ id , βˆ€π‘“.(T𝑖 βŠ“ B) βŠ‘ (T𝑗 βŠ“ C) : β„Ž β†’ id , (9’) βˆ€π‘“.(T𝑖 βŠ“ C) βŠ‘ (T𝑗 βŠ“ A) : π‘˜ β†’ id , βˆ€(𝑑𝑖 , 𝑑𝑗 ) ∈ / 𝐻, However, now the standard tiling argument applies and also yields undecidability. 3.1. Typed Mixed Case We observe from the previous section that inconsistent semantics for two instances of the same PD leads to undecidability. In this section, we show that under a restricted form of the mixed semantics, called the typed mixed semantics, set-π’Ÿβ„’β„±π’Ÿβ„ regains EXPTIME-completeness. The idea of enforcing a type restriction is to make the semantics of path agreements consistent among PDs ending with the same (inverse) feature. This type restrictions preserves the two-tree property of set-π’Ÿβ„’β„±π’Ÿβ„ under the set intersection and non-empty set equality semantics. Definition 6 (Type Restriction). Let 𝒯 be a set-π’Ÿβ„’β„±π’Ÿβ„ TBox and 𝒬 a posed question. Let end(Pd) denote the last (inverse) feature of Pd. We say that 𝒯 and 𝒬 are type restricted if for any pair of PDs Pd∼ 1 1 ∼2 and Pd2 in 𝒯 βˆͺ 𝒬, we have ∼1 , ∼2 ∈ {β‰ˆ, ∩} and end(Pd∼ ∼2 1 ) = end(Pd2 ) implies ∼1 =∼2 . 1 The typed mixed semantics immediately follow from the syntactic type restriction on all PDs in the TBox and posed question. Theorem 7. Let 𝒯 be a set-π’Ÿβ„’β„±π’Ÿβ„ TBox and 𝒬 a posed question, where 𝒯 βˆͺ 𝒬 are type restricted. Then the logical consequence problem 𝒯 |= 𝒬 is complete for EXPTIME. Proof (sketch): To establish the EXPTIME bound, we reduce the logical consequence problem to checking the unsatisfiability of an Ackermann formula [12] in a similar fashion as in [5]. First, we show that if there exists a counterexample ℐ for 𝒯 |= 𝒬, then we can construct a two-tree counterexample by unravelling ℐ. Note that under the imposed type discipline, there is only one form of path agreement applicable to any symmetric pair of individuals in the two-tree unravelling of ℐ and therefore there is no longer any need feature agreements that go beyond the symmetric agreements generated by PDDs. Since we can check the (un)satisfiability of the constructed Ackermann formula in EXPTIME [13], the same bound applies to the logical consequence problem for set-π’Ÿβ„’β„±π’Ÿβ„. β–‘ 4. Summary The paper explores the computational complexity of logical consequence for a new member of the FunDL family of descriptions logics called set-π’Ÿβ„’β„±π’Ÿβ„. This new dialect introduces a PDD concept constructor for capturing a richer variety of equality generating dependencies under arbitrary combinations of set intersection semantics and non-empty set equality semantics for path agreements in component path descriptions. In particular, the paper shows that an unconstrained option for choosing either semantics makes logical consequence undecidable. This is in contrast to the two cases where one or the other semantics is chosen exclusively for a given TBox which has been shown decidable in earlier work. The paper then proposes a typing discipline on path agreements to regain decidability, thereby accommodating some form of mixed-mode semantics for PDDs occurring in a given TBox. Future Work There are four main directions for further inquiry: 1. Adding arbitrary PDL-style test concepts [14] in path descriptions. In the case of PDDs this means adding concepts of the form (𝐢1 , 𝐢2 )?, stating that for a path agreement to hold, the paths from the two objects, π‘₯ and 𝑦, in the PDD constructor must simultaneously pass through an individual that belongs to 𝐢1 and 𝐢2 , respectively. We conjecture that adding such test concepts to path descriptions in set-π’Ÿβ„’β„±π’Ÿβ„ will not change the computational properties of the logic. 2. Studying additional or alternative notions of path agreement in set-π’Ÿβ„’β„±π’Ÿβ„. For example, the set intersection semantics of path agreements can be generalized by requiring the intersection to be of a certain cardinality (e.g., at least two or a majority of paths agree). We conjecture that such extensions will again lead to undecidability of entailment. 3. Studying set-π’Ÿβ„’β„±π’Ÿβ„ fragments with preferable computational properties, such as various Horn fragments. This direction suggests the use of (perhaps limited) PDDs in FunDL-Lite logics [4]. 4. Using PDD constructs in plural entity identification. While our introductory example has already sketched such a use case, the full consequences of using path descriptions in place of path functions are yet to be explored. References [1] A. Borgida, D. Toman, G. Weddell, On referring expressions in query answering over first order knowledge bases, in: Proc. Principles of Knowledge Representation and Reasoning, KR 2016, 2016, pp. 319–328. [2] A. Borgida, D. Toman, G. E. Weddell, On referring expressions in information systems derived from conceptual modelling, in: I. Comyn-Wattiau, K. Tanaka, I. Song, S. Yamamoto, M. Saeki (Eds.), Conceptual Modeling - 35th International Conference, ER 2016, volume 9974 of Lecture Notes in Computer Science, 2016, pp. 183–197. [3] D. Toman, G. E. Weddell, Using feature-based description logics to avoid duplicate elimination in object-relational query languages, KΓΌnstliche Intell. 34 (2020) 355–363. URL: https://doi.org/10. 1007/s13218-020-00666-7. doi:10.1007/s13218-020-00666-7. [4] S. McIntyre, D. Toman, G. E. Weddell, FunDL - A family of feature-based description logics, with applications in querying structured data sources, in: Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019, pp. 404–430. [5] E. Feng, A. Borgida, E. Franconi, P. F. Patel-Schneider, D. Toman, G. E. Weddell, Path description dependencies in feature-based dls, in: Description Logics, volume 3515 of CEUR Workshop Proceedings, CEUR-WS.org, 2023. [6] A. Borgida, E. Franconi, D. Toman, G. E. Weddell, Understanding document data sources using ontologies with referring expressions, in: H. Aziz, D. CorrΓͺa, T. French (Eds.), AI 2022: Advances in Artificial Intelligence - 35th Australasian Joint Conference, AI 2022, Perth, WA, Australia, December 5-8, 2022, Proceedings, volume 13728 of Lecture Notes in Computer Science, Springer, 2022, pp. 367–380. [7] D. Toman, G. Weddell, On Keys and Functional Dependencies as First-Class Citizens in Description Logics, in: Proc. of Int. Joint Conf. on Automated Reasoning (IJCAR), 2006, pp. 647–661. [8] D. Toman, G. E. Weddell, On keys and functional dependencies as first-class citizens in description logics, J. Aut. Reasoning 40 (2008) 117–132. [9] D. Toman, G. E. Weddell, On the interaction between inverse features and path-functional dependencies in description logics, in: Proc. Int. Joint Conf. on Artificial Intelligence (IJCAI), 2005, pp. 603–608. [10] D. Toman, G. Weddell, On Attributes, Roles, and Dependencies in Description Logics and the Ackermann Case of the Decision Problem, in: Description Logics 2001, CEUR-WS vol.49, 2001, pp. 76–85. [11] J. Hopcroft, J. Ullman, Introduction to Automata Theory, Languages and Computation, Addison- Wesley, 1979. [12] W. Ackermann, Uber die Erfullbarkeit gewisser Zahlausdrucke, Mathematische Annalen 100 (1928) 638–649. [13] M. FΓΌrer, Alternation and the Ackermann Case of the Decision Problem, L’Enseignement Math. 27 (1981) 137–162. [14] M. J. Fischer, R. E. Ladner, Propositional dynamic logic of regular programs, J. Comput. Syst. Sci. 18 (1979) 194–211.