Definite descriptions, along with individual names, have been recently introduced in the context of description logic languages, enriching the expressivity of standard nominal constructors. Moreover, in the first-order modal logic literature, definite descriptions have been widely investigated for their non-rigid behaviour, which allows them to denote diferent objects at diferent states. In this direction, we introduce epistemic and temporal extensions of standard description logics, with nominals and the universal role, additionally equipped with definite descriptions constructors. In the absence of the rigid designator assumption, we show that the satisfiability problem for epistemic free description logics is NExpTime-complete, while satisfiability for temporal free description logics over linear time structures is undecidable.
Definite descriptions , like ‘the smallest planet in the Solar System’, are expressions having form
‘the such that ’. Together with individual names, such as ‘Mercury’, they are used as referring
expressions to identify objects in a given domain [
In modal settings, such as temporal or epistemic, referring expressions can also behave as
non-rigid designators, meaning that they can denote diferent individuals across diferent states
(epistemic alternatives, instants of time, etc.). For this reason, non-rigid descriptions and names
have been widely investigated in first-order modal and temporal logics [
In this paper, we extend the free DLs proposed for the non-modal case in [
Proof details and examples are provided in an extended version of this article [28].
The DL S5ℒ is a modalised extension of the free DL ℒ [
axiom, denoting either a concept inclusion (CI ) of the form ⊑ , or an S5ℒ assertion of the form ( ) or ( 1, 2), where , are concepts, ∈ NR, and , 1, 2 are terms. A term of the form is called a definite description , and a concept { } is a (term) nominal. All the usual syntactic abbreviations are assumed, such as those for the box operator, 2 = ¬◇¬, and for the reflexive versions, ◇+ = ⊔ ◇ and 2+ = ⊓ 2.
Given an epistemic frame F = (, ∼ ), with being a non-empty set of worlds (or states) and ∼ ⊆ × being an equivalence relation on , a partial epistemic interpretation based on F is a triple M = (F, ∆ , ℐ), where: F is the frame of M; ∆ is a non-empty set, called the domain of M (we adopt the so-called constant domain assumption [27]); and ℐ is a function associating with every ∈ a partial interpretation ℐ = (∆ , · ℐ ) that maps every ∈ NC to a subset of ∆ , every ∈ NR to a subset of ∆ × ∆ , the universal role to the set ∆ × ∆ itself, and every in a subset of NI to an element in ∆ . In other words, every · ℐ is a total function on NC ∪ NR and a partial function on NI. We say that M = (F, ∆ , ℐ) is a total epistemic interpretation if every ℐ, with ∈ , is a total interpretation, meaning that · ℐ is defined as above, except that it maps every ∈ NI to an element of ∆ .
Given M = (F, ∆ , ℐ), with F = (, ∼ ), we say that M satisfies the rigid designator assumption (RDA) if, for every individual name ∈ NI and every , ∈ , the following condition holds: if ℐ is defined, then ℐ = ℐ , i.e., is a rigid designator. An individual name ∈ NI is said to denote in ℐ if ℐ is defined, and we say that it denotes in M if denotes in ℐ, for some ∈ . Moreover, is called a ghost in M if, for every ∈ , does not denote in ℐ. Dropping the RDA is the most general assumption, since rigid designators can be enforced by the CI, ◇+{} ⊑ 2+{}. Also, partial interpretations generalise the classical ones: an individual can be forced to denote at some state (i.e., not being a ghost) with the CI, ⊤ ⊑ ◇+∃.{}, and at all states by the formula, 2+(⊤ ⊑ ∃.{}). Note that a ghost individual is vacuously rigid.
Given M = (F, ∆ , ℐ), with F = (, ∼ ), and a world ∈ , we define the value ℐ of a term in as ℐ , if = , and as follows, for = : ( )ℐ = , if ℐ = {}, for some ∈ ∆ ; and undefined, otherwise. As for the extension of a concept in , ℐ is as usual with the following additions: (◇)ℐ = { ∈ ∆ | ∃ ∈ , ∼ : ∈ ℐ }, { }ℐ = {︃{ ℐ }, if denotes in ℐ, ∅, otherwise, where a term is said to denote in ℐ if ℐ is defined. A concept is satisfied at of M if ℐ ̸= ∅. An S5ℒ formula is satisfied at of M, written M, |= , when:
M, |= ( ) if denotes in ℐ and ℐ ∈ ℐ ,
M, |= ( 1, 2) if 1, 2 denotes in ℐ and ( 1ℐ , 2ℐ ) ∈ ℐ , M, |= ⊑ if ℐ ⊆ ℐ ,
M, |= ◇ if ∃ ∈ , ∼ : M, |= , together with the usual interpretation of Boolean operators. An S5ℒ formula is satisfied in M if there exists a world in M such that M, |= , and it is partial (total) satisfiable if there is a partial (total) modal interpretation M such that is satisfied in M.
For the temporal DL LTLℒ , we build LTLℒ terms, concepts, and formulas similarly to the S5ℒ case, by using the temporal operator until, , for the construction of concepts, , and formulas, . LTLℒ is obtained by disallowing descriptions. The flow of time is F = (N, <), where N is the set of natural number and < is the linear order on N. A partial temporal interpretation, or partial trace, based on F, is a triple M = (F, ∆ , ℐ), defined as in the epistemic case. We similarly define the notion of total trace. Given a partial trace M = (F, ∆ , ℐ), with F = (N, <) and ∈ N (that we call an instant of M), the value of an LTLℒ term at , the extension of an LTLℒ concept at , the satisfaction of a LTLℒ formula at , are defined as for the modal case, by replacing the semantics of the ◇ modal operator with the following one for the temporal operator: ( )ℐ = { ∈ ∆ | there is ∈ , < : ∈ ℐ and, for all ∈ (, ), ∈ ℐ },
M, |= if there is ∈ , < : M, |= and, for all ∈ (, ), M, |= . An LTLℒ formula (respectively, a concept ) is (partial or total) satisfiable , respectively, if (respectively, ) is satisfied at instant 0 in some (partial or total) trace M, respectively.
Assertions are syntactic sugar, since ( ) and ( 1, 2) are captured by the following CIs,
respectively: ⊤ ⊑ ∃.{ }, { } ⊑ ; and ⊤ ⊑ ∃.{ 1}, { 1} ⊑ ∃.{ 2}. To avoid ambiguities,
we use parentheses when applying Boolean or modal operators to assertions. Thus, for instance,
the formulas ¬(( )) and ◇(( )) abbreviate, respectively, ¬(⊤ ⊑ ∃.{ } ∧ { } ⊑ ) and
◇(⊤ ⊑ ∃.{ } ∧ { } ⊑ ), whereas the assertions ¬( ) and ◇( ) stand, respectively,
for ⊤ ⊑ ∃.{ } ∧ { } ⊑ ¬ and ⊤ ⊑ ∃.{ } ∧ { } ⊑ ◇. Finally, as already observed
for ℒ [
We also remark on a counter-intuitive behaviour without the RDA assumption. Let us consider the following formula: ({} ⊑ 2) ∧ ◇({} ⊑ ¬). This formula, while unsatisfiable if the RDA is assumed, is satisfiable without the RDA, since it is satisfied in an epistemic or temporal interpretation that interprets the individual name diferently in diferent states.
On S5ℒ satisfiability, we show the following, by adapting a quasimodel technique [27] to cover the case of possibly uninterpreted individual names not constrained by the RDA. Theorem 1. Partial S5ℒ formula satisfiability without the RDA is NExpTime-complete.
Concerning LTLℒ satisfiability, we have the following negative results, the proof of which is based on Degtyarev et al. [31] (related results appear also in Hampson and Kurucz [32]). Theorem 2. Formula satisfiability in LTLℒ without the RDA, and in LTLℒ with RDA, is undecidable.
Undecidability holds already for total satisfiability. Similar results apply also to LTL , ℒ interpreted on finite traces (using the standard translation of temporal DLs into temporal firstorder logic [27], and the reduction of the latter satisfiability from finite to infinite traces [33]).
We conducted a preliminary study on modal free description logics, in particular on the epistemic free DL S5ℒ , and on the temporal free DL LTLℒ . Syntactically, these DLs extend the classical ℒ, with nominals and the universal role, by including definite descriptions and epistemic or temporal operators. Semantically, we interpret these DLs over modal interpretations that allow for non-denoting terms and non-rigid designators. We show that, while formula satisfiability is NExpTime-complete for S5ℒ , it becomes undecidable for LTLℒ .
On the epistemic side, as future work we plan to: (i) consider frames for the propositional modal logics K4, T, S4, or KD45, to model diferent doxastic or epistemic attitudes [ 27]; (ii) investigate non-rigid descriptions and names in the context of non-normal modal DLs [34, 35, 36], to avoid the logical omniscience problem (i.e., an agent knows all the logical truths and all the consequences of their background knowledge), which afects all the systems extending K [37, 38]; (iii) address less expressive DL languages, such as ℰ ℒ , in an epistemic setting, and connect them with the recently investigated standpoint DL family [39, 40].
On the temporal side, we believe that the negative results presented here do not entirely undermine the use of definite descriptions on a temporal dimension. For applications in temporal conceptual modelling and ontology-mediated query answering [41, 42], it is worth exploring whether more encouraging results can be obtained in fragments restricting the use of temporal operators (limited, e.g., to the 2 operator only), or constraining the DL dimension (as in LTLℒ , without the universal role, or in the TDL-Lite family [43]).
Finally, we are interested in studying in this setting the complexities of other problems
than formula satisfiability. Related to interpolant and explicit definition existence [44, 45, 46],
the referring expression existence problem [
Andrea Mazzullo acknowledges the support of the MUR PNRR project FAIR - Future AI Research (PE00000013) funded by the NextGenerationEU. [15] F. Kröger, S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer
Science. An EATCS Series, Springer, 2008. [16] M. Fitting, R. L. Mendelsohn, First-order Modal Logic, Springer Science & Business Media, 2012. [17] G. Corsi, E. Orlandelli, Free quantified epistemic logics, Studia Logica 101 (2013) 1159–1183. [18] A. Indrzejczak, Existence, definedness and definite descriptions in hybrid modal logic, in: Proceedings of the 13th Conference on Advances in Modal Logic (AiML-20), College Publications, 2020, pp. 349–368. [19] E. Orlandelli, Labelled calculi for quantified modal logics with definite descriptions, J. Log.
Comput. 31 (2021) 923–946. [20] A. Mehdi, S. Rudolph, Revisiting semantics for epistemic extensions of description logics, in: Proceedings of the 25th AAAI Conference on Artificial Intelligence (AAAI-11), AAAI Press, 2011. [21] F. Wolter, M. Zakharyaschev, Temporalizing description logics, in: Proceedings of the 2nd International Symposium on Frontiers of Combining Systems (FroCoS-98), Research Studies Press/Wiley, 1998, pp. 104–109. [22] A. Artale, E. Franconi, Temporal description logics, in: Handbook of Temporal Reasoning in Artificial Intelligence, volume 1 of Foundations of Artificial Intelligence , Elsevier, 2005, pp. 375–388. [23] C. Lutz, F. Wolter, M. Zakharyaschev, Temporal description logics: A survey, in: Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME-08), IEEE Computer Society, 2008, pp. 3–14. [24] F. M. Donini, M. Lenzerini, D. Nardi, W. Nutt, A. Schaerf, An epistemic operator for description logics, Artif. Intell. 100 (1998) 225–274. [25] D. Calvanese, G. D. Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Inconsistency tolerance in P2P data integration: An epistemic logic approach, Inf. Syst. 33 (2008) 360–384. [26] M. Console, M. Lenzerini, Epistemic integrity constraints for ontology-based data management, in: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI-20), AAAI Press, 2020, pp. 2790–2797. [27] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics:
Theory and Applications, North Holland Publishing Company, 2003. [28] A. Artale, A. Mazzullo, Non-Rigid Designators in Epistemic and Temporal Free Description Logics (Extended Version), CoRR abs/2308.08640 (2023). URL: http://arxiv.org/abs/2308. 08640. [29] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider (Eds.), The Description Logic Handbook: Theory, Implementation, and Applications, Cambridge University Press, 2003. [30] S. Rudolph, Foundations of description logics, in: Tutorial Lectures of the 7th International Summer School 2011 on Reasoning Web, volume 6848 of Lecture Notes in Computer Science, Springer, 2011, pp. 76–136. [31] A. Degtyarev, M. Fisher, A. Lisitsa, Equality and monodic first-order temporal logic, Studia
Logica 72 (2002) 147–156. [32] C. Hampson, A. Kurucz, Undecidable propositional bimodal logics and one-variable ifrst-order linear temporal logics with counting, ACM Trans. Comput. Log. 16 (2015) 27:1–27:36. [33] A. Artale, A. Mazzullo, A. Ozaki, First-order temporal logic on finite traces: Semantic properties, decidable fragments, and applications, CoRR abs/2202.00610 (2022). [34] T. Dalmonte, A. Mazzullo, A. Ozaki, On non-normal modal description logics, in: M. Simkus,
G. E. Weddell (Eds.), DL, volume 2373, CEUR-WS.org, 2019. [35] T. Dalmonte, A. Mazzullo, A. Ozaki, Reasoning in non-normal modal description logics, in: C. Benzmüller, J. Otten (Eds.), ARQNL@IJCAR, volume 2095, 2022, pp. 28–45. [36] T. Dalmonte, A. Mazzullo, A. Ozaki, N. Troquard, Non-normal modal description logics, in: Proceedings of the the 18th European Conference on Logics in Artificial Intelligence (JELIA-23), to appear, 2023. [37] M. Y. Vardi, On epistemic logic and logical omniscience, in: J. Y. Halpern (Ed.), Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK-86), Morgan Kaufmann, 1986, pp. 293–305. [38] M. Y. Vardi, On the complexity of epistemic reasoning, in: Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS-89), IEEE Computer Society, 1989, pp. 243–252. [39] L. Gómez Álvarez, S. Rudolph, H. Strass, How to agree to disagree - managing ontological perspectives using standpoint logic, in: Proceedings of the 21st International Semantic Web Conference (ISWC-22), volume 13489, 2022, pp. 125–141. [40] L. Gómez Álvarez, S. Rudolph, H. Strass, Tractable diversity: Scalable multiperspective ontology management via standpoint EL, CoRR abs/2302.13187 (2023). [41] A. Artale, E. Franconi, F. Wolter, M. Zakharyaschev, A temporal description logic for reasoning over conceptual schemas and queries, in: Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA-02), volume 2424 of Lecture Notes in Artificial Intelligence , Springer-Verlag, 2002, pp. 98–110. [42] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Ontology-mediated query answering over temporal data: A survey (invited talk), in: Proceedings of the 24th International Symposium on Temporal Representation and Reasoning, (TIME-17), volume 90 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, pp. 1:1–1:37. [43] A. Artale, R. Kontchakov, V. Ryzhikov, M. Zakharyaschev, A cookbook for temporal conceptual data modelling with description logics, ACM Trans. Comput. Log. 15 (2014) 25:1–25:50. [44] A. Artale, J. C. Jung, A. Mazzullo, A. Ozaki, F. Wolter, Living without beth and craig: Definitions and interpolants in description logics with nominals and role inclusions, in: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI-21), AAAI Press, 2021, pp. 6193–6201. [45] A. Artale, J. C. Jung, A. , Mazzullo, A. Ozaki, F. Wolter, Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions, ACM Trans. Comput. Log. Online (Just Accepted) (2023). [46] A. Kurucz, F. Wolter, M. Zakharyaschev, Definitions and (uniform) interpolants in firstorder modal logic, CoRR abs/2303.04598 (2023).