An Update on Non-Rigid Designators in Modalised Description Logics (Extended Abstract) Alessandro Artale1 , Roman Kontchakov2 , Andrea Mazzullo1,3 and Frank Wolter4 1 Free University of Bozen-Bolzano, Piazza Domenicani, 3, Bolzano, 39100, Italy 2 Birkbeck, University of London, Malet St., London WC2E 7HX, UK 3 University of Trento, Via Sommarive, 9, Povo, 38123, Italy 4 University of Liverpool, Ashton Building, Ashton Street, Liverpool L69 3BX, UK Abstract We investigate decidability and complexity of the satisfaction problem for modal free description logics with non-rigid designators, which have recently been introduced as a powerful extension of standard modalised description logics. Our three main contributions are as follows. First, we systematically link the satisfiability problem for the one-variable fragment of first-order modal logic with counting to modal description logics with non-rigid designators. This enables us to transfer both negative and positive results from logics with counting to logics with non-rigid designators. Second, we prove a promising NExpTime upper bound for concept satisfiability for the fundamental epistemic multi-agent logic, S5𝑛 , and various neighbours. Finally, we conduct a fine-grained analysis of the decidability of temporal logics with non-rigid designators. Keywords Epistemic and temporal description logics, Definite descriptions, Non-rigid designators 1. Introduction Definite descriptions and individual names that are not rigid across worlds or time points have been one of the main research topics in first-order modal and temporal logics [1, 2, 3, 4, 5, 6, 7, 8, 9]. Recently, also a modal description logic (DL) formalism admitting non-rigid definite descriptions has been introduced [10]. While for first-order modal logics with rigid designators and no counting the restriction to monodic formulas (in which modal operators are only applied to formulas with a single free variable) very often ensures decidability, this is no longer the case if non-rigid designators and/or some counting are admitted [11]. For modal DLs, this implies that the standard recipe for designing decidable languages β€” apply modal operators only to concepts β€” does not always work anymore. Here, we explore in detail when this recipe still works, and when it does not. This paper is an extended abstract of [12]; see [13] for full details and proofs. Our first contribution closely links the two main sources of bad computational behaviour: non-rigid designators and counting. This enables us to use the results and machinery introduced for logics with counting [14, 15, 16]. We emphasise that the non-rigidity of symbols is not, by itself, the main source of difficulty. For instance, rigid roles are known to often cause an increase in the hardness of the satisfiability problem compared with the case of non-rigid roles only [11]. What makes non-rigid designators computationally harder is their ability to count in an unbounded way across worlds. On the other hand, we prove that, rather surprisingly, for some fundamental modal epistemic logics, non-rigid designators come for free: concept satisfiability for DLs based on K𝑛 and S5𝑛 is in NExpTime and thus not harder than without nominals at all. Finally, we show that undecidability is a relatively widespread phenomenon in the temporal setting: most combinations are undecidable (or even Ξ£11 -complete), and concept satisfiability is decidable only in fragments with the β€˜next time’ operator, where we obtain an ExpTime upper complexity bound, or in the expanding domain case with finite time, where the problem is actually Ackermann-hard. DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway " artale@inf.unibz.it (A. Artale); roman@dcs.bbk.ac.uk (R. Kontchakov); andrea.mazzullo@unibz.it (A. Mazzullo); wolter@liverpool.ac.uk (F. Wolter) Β© 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 2. Preliminaries The β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ language is a modalised extension of the free DL π’œβ„’π’žπ’ͺπ‘’πœ„ [17]. β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ terms and concepts are defined by the following grammar: 𝜏 ::= π‘Ž | πœ„πΆ, 𝐢 ::= 𝐴 | {𝜏 } | ¬𝐢 | (𝐢 βŠ“ 𝐢) | βˆƒπ‘Ÿ.𝐢 | βˆƒπ‘’.𝐢 | ◇𝑖 𝐢, where π‘Ž ranges over individual names, 𝐴 over concept names, π‘Ÿ over role names, ◇𝑖 over a finite set 𝐼 = {1, . . . , 𝑛} of modalities, and 𝑒 is the universal role. A term of the form πœ„πΆ is called a definite description. An β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ concept inclusion (CI ) is an expression of the form 𝐢 βŠ‘ 𝐷, for concepts 𝐢, 𝐷. An β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ ontology π’ͺ is a finite set of CIs. A frame is a pair F = (π‘Š, {𝑅𝑖 }π‘–βˆˆπΌ ), where π‘Š is a non-empty set of worlds (or states) and each 𝑅𝑖 βŠ† π‘Š Γ— π‘Š , for 𝑖 ∈ 𝐼, is a binary accessibility relation on π‘Š . A partial interpretation with expanding domains based on F is a triple M = (F, Ξ”, ℐ), where Ξ” is a function associating with every 𝑀 ∈ π‘Š a non-empty set, Δ𝑀 , called the domain of 𝑀 in M, such that Δ𝑣 βŠ† Δ𝑒 , whenever 𝑣𝑅𝑖 𝑒, for some 𝑖 ∈ 𝐼; and ℐ is a function associating with every 𝑀 ∈ π‘Š a partial DL interpretation ℐ𝑀 = (Δ𝑀 , ·ℐ𝑀 ) that maps every 𝐴 to a subset 𝐴ℐ𝑀 of Δ𝑀 , every π‘Ÿ to a subset π‘Ÿβ„π‘€ of Δ𝑀 Γ— Δ𝑀 , and a subset of the individual names π‘Ž to elements π‘Žβ„π‘€ in Δ𝑀 . Hence, every ℐ𝑀 is a total function on concept and role names, but a partial function on individual names. If ℐ𝑀 is defined on π‘Ž, then we say that π‘Ž designates at 𝑀. We say that M is a total interpretation if every π‘Ž designates at every 𝑀 ∈ π‘Š . Note that we do not assume that π‘Žβ„π‘€ = π‘Žβ„π‘£ , for 𝑀, 𝑣 ∈ π‘Š , and thus do not make the rigid designator assumption (RDA). An interpretation with constant domains is such that Δ𝑀 = Δ𝑣 , for all 𝑀, 𝑣 ∈ π‘Š . We define the value 𝜏 ℐ𝑀 of a term 𝜏 at 𝑀 ∈ π‘Š as π‘Žβ„π‘€ , for 𝜏 = π‘Ž, and as follows, for 𝜏 = πœ„πΆ: {οΈƒ ℐ𝑀 𝑑, if 𝐢 ℐ𝑀 = {𝑑}, for some 𝑑 ∈ Δ𝑀 ; (πœ„πΆ) = undefined, otherwise. A term 𝜏 is said to designate at 𝑀 if 𝜏 ℐ𝑀 = 𝑑, for some 𝑑 ∈ Δ𝑀 . The extension 𝐢 ℐ𝑀 of a concept 𝐢 in 𝑀 ∈ π‘Š is defined as usual, with the following variant: {οΈƒ {𝜏 ℐ𝑀 }, if 𝜏 designates at 𝑀, {𝜏 }ℐ𝑀 = βˆ…, otherwise. A concept 𝐢 is satisfied at 𝑀 ∈ π‘Š in M if 𝐢 ℐ𝑀 ΜΈ= βˆ…; 𝐢 is satisfied in M if it is satisfied at some 𝑀 ∈ π‘Š in M. A CI 𝐢 βŠ‘ 𝐷 is satisfied in M if 𝐢 ℐ𝑀 βŠ† 𝐷ℐ𝑀 , for every 𝑀 ∈ π‘Š . An ontology π’ͺ is satisfied in M if every CI in π’ͺ is satisfied in M; we also say a concept 𝐢 is satisfied in M under an ontology π’ͺ if M |= π’ͺ and 𝐢 ℐ𝑀 ΜΈ= βˆ…, for some 𝑀 ∈ π‘Š . Let π’ž be a class of frames (e.g., with equivalence relations for S5𝑛 ). We consider the following two main reasoning problems. Concept π’ž-Satisfiability: Given an β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -concept 𝐢, is there an interpretation M based on a frame from π’ž such that 𝐢 is satisfied in M? Concept π’ž-Satisfiability under Global Ontology: Given an β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -concept 𝐢 and an β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -ontology π’ͺ, is there an interpretation M based on a frame from π’ž such that 𝐢 is satisfied in M under π’ͺ? We begin with some simple observations on the reductions between the satisfiability problems for different semantic conditions and languages. Proposition 1. In β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ , concept π’ž-satisfiability (under global ontology) in total interpretations is polytime-reducible to concept π’ž-satisfiability (under global ontology, respectively) in partial interpretations, and the other way round. The reductions work both with constant and with expanding domains. Proposition 2. Concept π’ž-satisfiability (under global ontology) in β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ is polytime-reducible to concept π’ž-satisfiability (under global ontology, respectively) in β„³β„’π‘›π’œβ„’π’žπ’ͺ𝑒 (i.e., the fragment without πœ„), both with constant and with expanding domains. Table 1 Concept satisfiability (under global ontology) for πΏπ’œβ„’π’žπ’ͺπ‘’πœ„ concept satisfiability concept sat. under global ontology modal logic 𝐿 const. domain expanding domains const. domain expanding domains K𝑛 , 𝑛 β‰₯ 1 NExp-complete NExp-complete undecidable ? S5 NExp-complete NExp-complete S5𝑛 , 𝑛 β‰₯ 2 NExp-complete undecidable K*𝑛 , 𝑛 β‰₯ 1 Ξ£11 -complete undecidable Ξ£11 -complete undecidable K𝑓 *𝑛 , 𝑛 β‰₯ 1 undecidable decidable, Ackermann-hard undecidable decidable, Ackermann-hard 3. Main Results Non-Rigid Designators and Counting We prove a strong link between non-rigid designators and the first-order one-variable modal logic enriched with the β€˜elsewhere’ quantifier, ℳℒ𝑛Diff [14, 15, 16], which can be introduced using DL-style syntax: 𝐢 ::= 𝐴 | ¬𝐢 | (𝐢 βŠ“ 𝐢) | βˆƒπ‘’.𝐢 | βˆƒΜΈ= 𝑒.𝐢 | ◇𝑖 𝐢, where 𝑖 ∈ 𝐼. Note that the language has no terms and no{οΈ€ roles apart from the universal role 𝑒. All constructs are interpreted as before and (βˆƒΜΈ= 𝑒.𝐢)ℐ𝑀 = 𝑑 ∈ Δ𝑀 | 𝐢 ℐ𝑀 βˆ– {𝑑} ΜΈ= βˆ… . Observe }οΈ€ that ℳℒ𝑛Diff can be regarded as a basic first-order modal logic}οΈ€with counting because the counting quantifier βˆƒ=1 𝑒.𝐢, with (βˆƒ=1 𝑒.𝐢)ℐ𝑀 = 𝑑 ∈ Δ𝑀 | |𝐢 ℐ𝑀 | = 1 , is equivalent to βˆƒπ‘’.(𝐢 βŠ“ Β¬βˆƒΜΈ= 𝑒.𝐢) {οΈ€ and, conversely, βˆƒΜΈ= 𝑒.𝐢 is equivalent to βˆƒπ‘’.𝐢 βŠ“ (𝐢 β‡’ Β¬βˆƒ=1 𝑒.𝐢). Theorem 3. π’ž-satisfiability of β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -concepts (under global ontology) can be reduced in double exponential time to π’ž-satisfiability of ℳℒ𝑛Diff -concepts (under global ontology, respectively), both with constant and with expanding domains. Conversely, π’ž-satisfiability of ℳℒ𝑛Diff -concepts (under global ontology) is polytime-reducible to π’ž- satisfiability of β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -concepts (under global ontology, respectively), both with constant and with expanding domains. Reasoning in Modal Free Description Logics Given a propositional modal logic 𝐿 with 𝑛 operators and the class π’žπΏ of frames validating 𝐿, we define πΏπ’œβ„’π’žπ’ͺπ‘’πœ„ concept satisfiability (under global ontology) as the problem of deciding π’žπΏ -satisfiability of β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ -concepts (under global ontology, respectively). For 𝐿 = K𝑛 , π’žπΏ is the class of all frames with 𝑛 relations; for 𝐿 = S5𝑛 , π’žπΏ is the class of frames with 𝑛 equivalence relations; for K*𝑛 , π’žπΏ is the class of all frames (π‘Š, 𝑅1 , . . . , 𝑅𝑛 , 𝑅) such that 𝑅 is the transitive closure of 𝑅1 βˆͺ Β· Β· Β· βˆͺ 𝑅𝑛 ; and for K𝑓 *𝑛 , π’žπΏ is as for K*𝑛 , with in addition π‘Š finite and 𝑅 irreflexive. (i.e., there is no chain 𝑀0 𝑅𝑖1 𝑀1 Β· Β· Β· 𝑅𝑖𝑛 𝑀𝑛 with 𝑀0 = 𝑀𝑛 ). We drop superscript 1 from 𝐿1 . Table 1 presents our main results for modal logics relevant in the epistemic context. The NExpTime membership for concept satisfiability in Kπ‘›π’œβ„’π’žπ’ͺπ‘’πœ„ and S5π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ is shown using the quasimodel technique: we prove that a concept is satisfiable iff there is a quasimodel of exponential size, which gives us the exponential finite model property and an exponential-time non-deterministic algorithm for concept satisfiability. Decidability of concept satisfiability under global ontology in K𝑓 *𝑛 π’œβ„’π’žπ’ͺπ‘’πœ„ is also shown with quasimodels. In this case, we count the number of times a type occurs in a world and represent quasistates as vectors with elements in N βˆͺ {∞}. Then Dickson’s Lemma is used to obtain a computable bound on the size of a satisfying interpretation. Note, however, that Ackermann-hardness, which follows by a non-trivial reduction from a result on ℳℒ𝑛Diff [15], shows that the interpretation size is not bounded by a primitive recursive function. Many challenging open problems remain, in particular, decidability of K𝑛 under global ontology and expanding domains, as well as decidability of logics of transitive frames, e.g., K4. As a first step, we show decidability with expanding domains for the GΓΆdel-LΓΆb provability logic GL (whose transitive and irreflexive frames have no infinite ascending chains) and its reflexive companion Grzegorczyk (Grz), using reductions to expanding-domains products [18]. Table 2 Concept satisfiability (under global ontology) for πΏπ’œβ„’π’žπ’ͺπ‘’πœ„ concept satisfiability concept sat. under global ontology temporal logic 𝐿 const. domain expanding domains const. domain expanding domains LTLβ—‡ , LTL Ξ£11 -complete undecidable Ξ£11 -complete undecidable LTL𝑓 β—‡ , LTL𝑓 undecidable decidable, Ackermann-hard undecidable decidable, Ackermann-hard LTL∘ Exp-complete Exp-complete undecidable ? LTL𝑓 ∘ Exp-complete Exp-complete undecidable decidable Reasoning in Temporal Free Description Logics For the temporal DL language 𝒯 β„’π’œβ„’π’žπ’ͺπ‘’πœ„ , we build 𝒯 β„’π’œβ„’π’žπ’ͺπ‘’πœ„ terms, concepts, concept inclusions and ontologies as in the β„³β„’π‘›π’œβ„’π’žπ’ͺπ‘’πœ„ case, with 𝑛 = 2: the language has two modalities β€” temporal operators β€˜sometime in the future’, β—‡, and β€˜at the next moment’, β—‹. In particular, the 𝒯 β„’π’œβ„’π’žπ’ͺπ‘’πœ„ concepts are defined by the following grammar: 𝐢 ::= 𝐴 | {𝜏 } | ¬𝐢 | (𝐢 βŠ“ 𝐢) | βˆƒπ‘Ÿ.𝐢 | βˆƒπ‘’.𝐢 | ◇𝐢 | ○𝐢. A flow of time F is a pair (𝑇, <), where 𝑇 is either the set N of non-negative integers or a subset of N of the form [0, 𝑛], for 𝑛 ∈ N, and < is the strict linear order on 𝑇 , which naturally gives rise to interpretations M based on corresponding frames. Given M, the value of a term 𝜏 at 𝑑 ∈ 𝑇 and the extension of a concept 𝐢 at 𝑑 ∈ 𝑇 are defined as in the modal case for 𝑛 = 2: for example, (○𝐷)ℐ𝑑 = {𝑑 ∈ Δ𝑑 | 𝑑 + 1 ∈ 𝑇 and 𝑑 ∈ 𝐷ℐ𝑑+1 }. In particular, the extension of ○𝐷 is empty in the last instant of a finite flow of time. Note that β—‡ is interpreted by < and thus does not include the current instant, but we can easily define β—‡+ 𝐢 = ◇𝐢 βŠ” 𝐢, which includes the current time instant. We also use standard abbreviations such as 2𝐢 (β€˜always in the future’) and 2+ 𝐢 (β€˜from now on’). Fragments 𝒯 β„’β—‡ ∘ π’œβ„’π’žπ’ͺπ‘’πœ„ and 𝒯 β„’π’œβ„’π’žπ’ͺπ‘’πœ„ are obtained from 𝒯 β„’π’œβ„’π’žπ’ͺ𝑒 by disallowing β—‹ and β—‡ operators, πœ„ respectively; they correspond to β„³β„’π’œβ„’π’žπ’ͺπ‘’πœ„ , but with different accessibility relations. We refer, for 1 instance, to the satisfiability problem for 𝒯 β„’β—‡ π’œβ„’π’žπ’ͺπ‘’πœ„ concepts in interpretations with finite flows of time β—‡ (𝑓 ) as LTL𝑓 π’œβ„’π’žπ’ͺπ‘’πœ„ concept satisfiability. Table 2 summarises our results. Concept satisfiability under global ontology for languages with the β—‡ operator is undecidable over (N, <) in both constant and expanding domains and over finite flows of time in constant domains. Positive results, however, can be obtained by combining finite flows of time with expanding domains, or by restricting to concept satisfiability in fragments with only the β—‹ operator. An interesting open problem is decidability of LTLβˆ˜π’œβ„’π’žπ’ͺπ‘’πœ„ concepts under global ontology in expanding domains. 4. Discussion and Future Work In this work, we have made first steps towards understanding the computational behaviour of non-rigid designators and definite descriptions in epistemic and temporal DLs. Potential applications include business process management where formalisms for representing the dynamic behaviour of data and information are crucial [19, 20, 21] and context, knowledge, or standpoint dependent reasoning for which possible worlds semantics is needed [22, 23]. Future research directions include the extension of our results to more expressive monodic fragments [11, 24], automated support for the construction of definite descriptions and referring expressions [17, 25], the design of β€˜practical’ reasoning algorithms for the languages considered here, and the extension of our results to non-normal modal DLs [26]. Acknowledgments Andrea Mazzullo acknowledges the support of the MUR PNRR project FAIR - Future AI Research (PE00000013) funded by the NextGenerationEU. References [1] N. B. Cocchiarella, Philosophical perspectives on quantification in tense and modal logic, in: Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, Springer, 1984, pp. 309–353. doi:10.1007/978-94-009-6259-0_6. [2] J. W. Garson, Quantification in modal logic, in: Handbook of philosophical logic, volume II: Extensions of Classical Logic, Springer, 1984, pp. 249–307. doi:10.1007/978-94-009-6259-0_ 5. [3] T. BraΓΌner, S. Ghilardi, First-order Modal Logic, in: Handbook of Modal Logic, Elsevier, 2007, pp. 549–620. doi:doi:10.1016/S1570-2464(07)80012-7. [4] F. KrΓΆger, S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2008. doi:10.1007/978-3-540-68635-4. [5] M. Fitting, R. L. Mendelsohn, First-order Modal Logic, Springer Science & Business Media, 2012. [6] G. Corsi, E. Orlandelli, Free quantified epistemic logics, Studia Logica 101 (2013) 1159–1183. doi:10.1007/S11225-013-9528-X. [7] A. Indrzejczak, Existence, definedness and definite descriptions in hybrid modal logic, in: Proc. of the 13th Conf. on Advances in Modal Logic, AiML-20, College Publications, 2020, pp. 349–368. URL: http://www.aiml.net/volumes/volume13/Indrzejczak.pdf. [8] E. Orlandelli, Labelled calculi for quantified modal logics with definite descriptions, J. Log. Comput. 31 (2021) 923–946. doi:10.1093/LOGCOM/EXAB018. [9] A. Indrzejczak, M. Zawidzki, Definite descriptions and hybrid tense logic, Synthese 202 (2023) 98. doi:10.1007/s11229-023-04319-8. [10] A. Artale, A. Mazzullo, Non-rigid designators in epistemic and temporal free description logics (extended abstract), in: Proc. of the 36th Int. Workshop on Description Logics, DL 2023, volume 3515 of CEUR Workshop Proceedings, CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3515/ abstract-4.pdf. [11] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics: Theory and Applications, North Holland Publishing Company, 2003. [12] A. Artale, R. Kontchakov, A. Mazzullo, F. Wolter, Non-Rigid Designators in Modal and Temporal Free Description Logics, in: Proc. of the 21st Int. Conf. on Principles of Knowledge Representation and Reasoning, KR-24, 2024. [13] A. Artale, R. Kontchakov, A. Mazzullo, F. Wolter, Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version), CoRR abs/2405.07656 (2024). arXiv:2405.07656. [14] C. Hampson, A. Kurucz, On modal products with the logic of ’elsewhere’, in: Proc. of the 9th Conf. on Advances in Modal Logic, AiML-12, College Publications, 2012, pp. 339–347. URL: http://www.aiml.net/volumes/volume9/Hampson-Kurucz.pdf. [15] C. Hampson, A. Kurucz, Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting, ACM Trans. Comput. Log. 16 (2015) 27:1–27:36. doi:10. 1145/2757285. [16] C. Hampson, Decidable first-order modal logics with counting quantifiers, in: Proc. of the 11th Conf. on Advances in Modal Logic, AiML-16, College Publications, 2016, pp. 382–400. URL: http://www.aiml.net/volumes/volume11/Hampson.pdf. [17] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On Free Description Logics with Definite Descriptions, in: Proc. of the 18th Int. Conference on Principles of Knowledge Representation and Reasoning, KR-21, 2021, pp. 63–73. doi:10.24963/KR.2021/7. [18] D. Gabelaia, A. Kurucz, F. Wolter, M. Zakharyaschev, Non-primitive recursive decidability of products of modal logics with expanding domains, Ann. Pure Appl. Log. 142 (2006) 245–268. doi:10.1016/J.APAL.2006.01.001. [19] J. P. Delgrande, B. Glimm, T. A. Meyer, M. Truszczynski, F. Wolter, Current and future challenges in knowledge representation and reasoning, CoRR abs/2308.04161 (2023). arXiv:2308.04161. [20] A. Deutsch, R. Hull, Y. Li, V. Vianu, Automatic verification of database-centric systems, ACM SIGLOG News 5 (2018) 37–56. doi:10.1145/3212019.3212025. [21] A. Artale, L. Geatti, N. Gigante, A. Mazzullo, A landscape of first-order linear temporal logics in infinite-state verification and temporal ontologies, in: Short Paper Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2023), volume 3629 of CEUR Workshop Proceedings, CEUR-WS.org, 2023, pp. 85–92. URL: https://ceur-ws.org/Vol-3629/paper14.pdf. [22] C. Ghidini, L. Serafini, Distributed first order logic, Artif. Intell. 253 (2017) 1–39. doi:10.1016/J. ARTINT.2017.08.008. [23] L. GΓ³mez Álvarez, S. Rudolph, H. Strass, Tractable diversity: Scalable multiperspective ontology management via standpoint EL, in: Proc. of the 32nd International Joint Conference on Artificial Intelligence, IJCAI 2023, ijcai.org, 2023, pp. 3258–3267. doi:10.24963/IJCAI.2023/363. [24] I. M. Hodkinson, F. Wolter, M. Zakharyaschev, Decidable and undecidable fragments of first-order branching temporal logics, in: Proc. of the 17th IEEE Symposium on Logic in Computer Science, LICS-02, IEEE Computer Society, 2002, pp. 393–402. doi:10.1109/LICS.2002.1029847. [25] A. Kurucz, F. Wolter, M. Zakharyaschev, Definitions and (uniform) interpolants in first-order modal logic, in: Proc. of the 20th Int. Conf. on Principles of Knowledge Representation and Reasoning, KR 2023, 2023, pp. 417–428. doi:10.24963/KR.2023/41. [26] T. Dalmonte, A. Mazzullo, A. Ozaki, N. Troquard, Non-normal modal description logics, in: Proc. of the 18th European Conference on Logics in Artificial Intelligence, JELIA 2023, volume 14281 of LNCS, Springer, 2023, pp. 306–321. doi:10.1007/978-3-031-43619-2\_22.