=Paper= {{Paper |id=Vol-3739/abstract-4 |storemode=property |title=An Update on Non-Rigid Designators in Modalised Description Logics (Extended Abstract) |pdfUrl=https://ceur-ws.org/Vol-3739/abstract-4.pdf |volume=Vol-3739 |authors=Alessandro Artale,Roman Kontchakov,Andrea Mazzullo,Frank Wolter |dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleKMW24 }} ==An Update on Non-Rigid Designators in Modalised Description Logics (Extended Abstract)== https://ceur-ws.org/Vol-3739/abstract-4.pdf 
                         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.