Definite descriptions are phrases of the form 'the x such that ''. Together with individual names, they are used to refer to single entities in a context. In some cases, however, names and descriptions may fail to denote any object at all, as witnessed by the name 'DL 1993', for a workshop that never took place, or the description 'the Special Session of DL 2020', for a non-occurring event. In this work, we introduce and investigate DL languages with individual names and definite descriptions which may both fail to denote. We focus on ALCO-based and ELO-based languages. A generic polynomial time reduction of the resulting expressive free DLs with definite descriptions into classical DLs is provided, and we show that free ELO with definite descriptions is still in PTime. Moreover, we characterise the expressive power of concepts relative to first-order formulas interpreted on partial interpretations using a suitable notion of bisimulation.
A noun phrase that can be used to refer to a single object in a context is known
in linguistics as a referring expression. These include both individual names,
such as ‘DL 2020’, and definite descriptions, such as ‘the General Chair of DL
2020’ [
When it comes to formalisation, however, this behaviour is not easily
captured in frameworks based on classical first-order logic, where an individual name
Copyright c 2020 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
is always assigned to an element of the domain by the interpretation function,
and definite descriptions are not included among the terms of the language. An
approach dating back to Russell [
In this work, we introduce and study a family of DL languages with both individual names and definite descriptions, that we call free DLs with definite descriptions, or free DLs, for short. Syntactically, these languages extend the classical ones with nominals of the form f Cg, where C is a term standing for the definite description ‘the object that is C’ and C is a concept. We denote the resulting DLs with an upperscript , focussing in particular on ALCO and E LO . Their semantics is based on partial interpretations, that generalise the classical ones by letting the interpretation function to be partial on individual names, meaning that only a subset of all the individual names has its elements assigned to objects of the domain. Moreover, the extension of f Cg in a partial interpretation coincides with that of the concept C, if C is interpreted as a singleton, and it is empty otherwise. This semantic choice respects the main tenets of Russell’s paraphrase, while also preserving definite descriptions as terms.
One motivation behind the introduction of this family of languages is to add, at the modelling level, the flexibility of empty-valued individual names, as well as the possibility to single out elements of a domain via definite descriptions. These additional features can also be used in the context of query answering over DL knowledge bases. For example, the Boolean instance queries >(dl93);
9isProgramChairOf:fdl09g( 9isGeneralChairOf:fdl20g); ask whether ‘DL 1993’ names anything at all, and whether the General Chair of DL 2020 was also a Program Chair of DL 2009, respectively. One can now retrieve not only individual names, but also definite descriptions as answers to queries. Moreover, nominals involving definite descriptions can be used to form concept inclusions with different satisfaction conditions. Consider for instance
The former, stating that every organiser of DL 2020 reports to the General Chair of DL 2020, forces 9isGeneralChairOf:fdl20g to have exactly one element in all its models satisfying 9organises:fdl20g. The latter holds if, whenever there is exactly one Program Chair of DL 2020, that individual selects some Reviewer, but also in interpretations without, or with more than one, Program Chair of DL 2020.
On the technical side, we show that reasoning in free DLs with definite descriptions can be performed at no additional costs. For (extensions of) ALCO , we employ a reduction to languages covered by the OWL 2 standard, so that efficient off-the-shelf reasoners can be used. In particular, we prove that satisfiability in ALCO can be polynomially reduced (via a translation that can be applied to other constructors as well) to ALCOu, i.e., ALCO extended with the universal role. Moreover, we show that entailment in E LO knowledge bases remains tractable, using a modified version of the algorithm for classical E LO. Finally, we focus on ALCO expressive power, showing that its concepts can be characterised in terms of first-order formulas on partial interpretations that are invariant under a suitable notion of bisimulation. We conclude the paper with a discussion of related work and future directions. 2
We introduce basic notions for free DLs (with definite descriptions) by presenting
the syntax and semantics of ALCO , which we define as a free DL based on the
classical DL ALCO [
Syntax Let NC, NR and NI be countably infinite and pairwise disjoint sets of concept names, role names, and individual names, respectively. The ALCO terms and concepts are constructed by mutual induction as follows: ::= a j C;
C ::= A j :C j (C u C) j 9r:C j f g; with a 2 NI, A 2 NC and r 2 NR. A term of the form C is called a definite description, and a concept f g is called a (term) nominal. An ALCO atom is either an ALCO concept inclusion (CI ) of the form C v D or an ALCO assertion of the form A( ) or r( 1; 2), where C; D are ALCO concepts, A 2 NC, r 2 NR, and ; 1; 2 are ALCO terms. An instance query is either an assertion or an expression of the form C( ), where C is an ALCO concept and is a term. We may omit ‘ALCO ’ if this is clear from the context. Thus, a TBox T is a finite set of CIs, an ABox A is a finite set of assertions, and a knowledge base (KB) K is a pair (T ; A). Although we are particularly interested in working with KBs, for the presentation of the results it is convenient to combine CIs and assertions into ALCO formulas, defined as expressions of the form ' ::=
j :' j (' ^ '); where is an atom. All the usual syntactic abbreviations and conventions are assumed. In particular, for concepts, we set ? = A u :A, > = :?, C t D = :(:C u:D), C ) D = :C tD, and 8r:C = :9r::C, while a concept equivalence (CE ) C D abbreviates C v D; D v C (as a formula, it stands for the conjunction of the two). The signature of ', ', is the set of all concept, role and individual names occurring in ', while con(') is the set of all concepts occurring in ' (and similarly for concepts, TBoxes, ABoxes and KBs).
In the rest of this paper, we will consider other DL languages with nominals,
that we introduce briefly here. Since ALCO nominals are constructed using
arbitrary terms, the classical ALCO is the sublanguage of ALCO where terms
can only be in NI. The language ALCOu extends ALCO with the universal role
u, allowing for concepts of the form 9u:C [
Semantics For the DL languages with nominals considered in this work, we introduce semantics that generalise the classical ones through the notion of partial interpretation. A partial interpretation is a pair I = ( I ; I ), where I is a non-empty set, called the domain of I, and I is a function that maps every A 2 NC to a subset of I , every r 2 NR to a subset of I I , the universal role u to the set I I itself, and every a in a subset of NI to an element in I . In other words, I is a total function on NC [ NR and a partial function on NI. A total interpretation is a partial interpretation I = ( I ; I ) in which I is also total on NI. The value I of a term in I and the extension CI of a concept C in I are defined by mutual induction: ( C)I = (d;
if CI = fdg; for some d 2 undefined; otherwise: I ; We say that denotes in I iff I = d, for a d 2 I . Thus, in particular, an individual name a denotes in I iff aI is defined. In addition: (:C)I =
I n CI ;
(C u D)I = CI \ DI ; (9r:C)I = fd 2
I j 9e 2 CI : (d; e) 2 rI g: Moreover, we set f gI = f I g, if denotes in I, and f gI = ;, otherwise.
A concept C is satisfied in I iff CI 6= ;, and it is satisfiable iff there is a partial interpretation in which it is satisfied. The satisfaction of an ALCO formula ' in I, written I j= ', is defined as follows. For CIs:
I j= C v D iff CI
DI : For instance queries (generalizing assertions):
I j= C( ) iff
denotes in I and I 2 CI ; I j= r( 1; 2) iff
1; 2 denote in I and ( 1I ; 2I ) 2 rI : Finally, for the remaining formulas:
I j= : iff We say that ' is satisfied in a partial interpretation I (or that I satisfies, or is a model of, ') iff I j= ', and that ' is satisfiable iff it is satisfied in some I. Moreover, ' entails , written ' j= , if every interpretation that satisfies ' satisfies also . Finally, ' and are equivalent iff they entail each other. As usual, the formula satisfiability problem is the problem of deciding whether a given formula is satisfied in some (partial) interpretation. The entailment problem is the problem of deciding whether a given formula entails another formula (or, in particular, an instance query). We may also consider these problems restricted to total interpretations and write ‘on total interpretations’ explicitly whenever this is the case. These notions extend naturally to TBoxes, ABoxes and KBs, as well as to other free DLs presented in subsequent sections.
Example 1. In the context of DL workshops, dl93 and dl20 are examples of, respectively, a non-denoting and a denoting individual name, while the definite description 9isGeneralChairOf:fdl20g denotes the General Chair of DL 2020. The following concept, applying to Program Chairs of DL 2020 that are not the only ones, shows an interaction between a nominal constructed from a definite description and the concept occurring inside it:
Let OneOfDL20ProgramChairs abbreviate the concept above. The CI
OneOfDL20ProgramChairs v 9collaboratesWith:9isProgramChairOf:fdl20g states that every DL 2020 Program Chair who is not the only one collaborates with someone who is a DL 2020 Program Chair. 2.3
First Observations We discuss some properties of free DLs. Our first observation is that the ALCO formula satisfiability problem on total interpretations can be reduced to the ALCO formula satisfiability problem on partial interpretations. This is because an ALCO term denotes in a partial interpretation I iff I j= :(f g v ?). An ALCO formula ' entails >( ) iff ' j= :(f g v ?) and this happens iff denotes in all the ALCO partial interpretations that are models of '. Then, to solve satisfiability on total interpretations, one can simply add conjuncts of the form :(f g v ?) for each individual name = a occurring in the formula.
Our second observation is that, due to partial interpretations, an instance query C( ) is not equivalent to f g v C. Indeed, while terms always denote in the models of the instance queries (and assertions) in which they occur, the CI f g v C is satisfied in any partial interpretation where is not denoting. Nevertheless, instance queries are just syntactic sugar: one can replace C( ) by f g v C ^ :(f g v ?); and r( 1; 2) by f 1g v 9r:f 2g ^ :(f 1g v ?). Thus, from now on, we may assume without loss of generality that ALCO formulas do not contain assertions. Also, deciding whether instance queries are entailed can be reduced to formula satisfiability. Observe that this encoding yields an equivalent formula. It is possible to obtain an equisatisfiable translation that is also expressible within the E LO fragment by replacing C( ) with CIs of the form > v 9s:f g, f g v C, and r( 1; 2) with > v 9s:f 1g, f 1g v 9r:f 2g, where s is a fresh role name.
Our third observation is regarding Boolean operators. CIs of the form f (C t D)g v f Cg t f Dg; f Cg u f Dg v f (C u D)g are satisfied in every partial interpretation (but the direction w may not hold).
Finally, we point out that, for satisfiability checking, it suffices to consider ALCO formulas where all occurrences of definite descriptions are of the form B, where B is a concept name. Indeed, let C1; : : : ; Cn be all the definite descriptions in ' that do not occur in the body of another definite description C0, where the body of a definite description C is just C. We define the ALCO formula '0 as the formula obtained by substituting the bodies C1; : : : ; Cn of C1; : : : ; Cn with fresh concept names BC1 ; : : : ; BCn , respectively. Then, '00 is defined as the ALCO conjunction: where (BC C)00 is the formula obtained by recursively applying the procedure just described to the CE BC C. It can be checked that ' and '00 are equisatisfiable ALCO formulas. Moreover, given '00, we assume without loss of generality that '00 does not contain any assertion (cf. second observation above). Finally, all the CIs occurring in '00 will be assumed without loss of generality to be either of the form E v F , where E; F are ALC concepts, or f g v A, or A v f g, with A 2 NC and either an individual name or of the form B, where B 2 NC. Indeed, given an ALCO CI C v D occurring in '00, we can obtain an equisatisfiable ALCO formula by substituting all nominals f g occurring in C v D with concept names A , and taking the conjunction of the resulting ALC CI with the CEs A f g. A formula in this format is said to be in normal form. 3
We analyse the complexity of reasoning in ALCO and in E LO . 3.1
Satisfiability in ALCO We prove that satisfiability in ALCO is ExpTime-complete. To show this result, we provide a polynomial size equisatisfiable translation into ALCOu. Given an ALCO formula ' in normal form, we define a translation of ' into an ALCOu formula ' . While the translation preserves concept and role names in NC [ NR, nominals f g are translated in the following way:
f g = f g+ u C 1; where f g+ = (
Ab; B; if if is of the form b 2 NI; is of the form B; with Ab fresh concept name, and C 1 stands for the concept 8u:(f g+ ) fa g); with a fresh individual name. We now define ' inductively as follows: (E v F ) = E v F; (f g v A) = f g v A;
(A v f g) = A v f g ; (: ) = : ;
+ v 8u:(fa g ) f g+): Lemma 1. An ALCO formula ' is satisfiable iff the ALCOu formula 'y is satisfiable on total interpretations.
It follows from a known result in Propositional Dynamic Logic extended with
nominals and the universal modality [35, Corollary 7.7] that the ALCOu formula
satisfiability problem is in ExpTime. The matching lower bound comes from the
ALC formula satisfiability problem [
The reduction we presented can be easily adapted to deal with more
expressive DLs, e.g., extensions of ALCO with inverse roles and number restrictions.
We prove that satisfiability of E LO formulas is NP-complete and entailment in
E LO KBs is PTime-complete. To show these results, we assume without loss of
generality that the ABox and instance queries can be encoded within the TBox
(cf. Subsection 2.3) and adapt the completion algorithm for E LO TBoxes [
Let T be an E LO TBox. We denote by BCT the union of f>g, the set of all concept names occurring in T , and the set of all concepts fag with a an individual name occurring in T . Also, we denote by BCT+ the union of BCT with f?g [ ff Ag j f Ag occurs in T g and by RT the set of role names occurring in T . We assume without loss of generality that any ELO TBox T is normalized and all CIs in it have one of the following forms:
C1 u C2 v D; 9r:C v D; C v 9r:D; f g v D;
D v f g; where C(i) 2 (BCT \ NC) [ f>g, D 2 (BCT \ NC) [ f>; ?g and all terms in a , with a 2 NI, or of the form f Ag, with A 2 NC.
T are either of the form f g Given A; B 2 NC, we may write A v B instead of A u A v B. Moreover, if f Ag occurs in T then we assume without loss of generality that f Ag v A 2 T .
The classification graph for T is a tuple (V; V V; S; R) where – V = BCT [ fAc j A 2 (BCT \ NC)g, with each Ac 2 NC fresh; + – S is a function mapping nodes in V to subsets of BCT ; – R is a function mapping edges in V V to (possibly empty) subsets of RT . Intuitively, a concept name of the form Ac represents a second element in the extension of A, and it is removed from the classification graph if A has at most one object in its extension. We write C ;R D iff there are C1; : : : ; Ck 2 BCT such that C1 = C; R(Cj; Cj+1) 6= ;, for all 1 j < k; Ck = D. One can show that the label sets satisfy the following invariants: – D 2 S(C) implies T j= C v D; and – r 2 R(C; D) implies T j= C v 9r:D.
Initially, we set S(C) := fC; >g for all nodes C 2 V , and R(C; D) := ; for all edges (C; D) 2 V V . If C 2 V n BCT is of the form Ac, with A 2 NC, then we add A to S(Ac). The above invariants are satisfied by these initial label sets. The completion rules are given in Table 1. Assume that rules are only applied if S or R or V change after the rule application. This bounds the number of rule applications to a polynomial in the number of concept and role names in T . We assume that A is a special concept name we want to check for satisfiability (it appears in Rule R10 of Table 1). To show that subsumption in ELO can be decided in polynomial time one needs to show that if no more rules are applicable, then T j= A v B iff B 2 S(A). We formalise this with Lemma 2. Lemma 2. Given a TBox T , let S be the node function of a complete classification graph for T (cf. rules in Table 1). Then, T j= A v B iff S(A) \ fB; ?g 6= ;.
Any ELO TBox T can be normalized (preserving satisfiability) in polynomial time and the classification graph for an ELO TBox T can be constructed in polynomial time with respect to the size of T . Then, given arbitrary ELO concepts C; D and an ELO TBox T , one can decide whether C v D is entailed by T by adding A C and B D to T , normalizing it, and then checking whether S(A) \ fB; ?g 6= ;, where A; B are fresh concept names (Lemma 2). As already mentioned, ABoxes can be encoded into the TBox and instance checking can be reduced to the entailment of CIs. Formula satisfiability can be divided into two problems: one is the satisfiability of a propositional formula obtained by replacing each CI with a fresh propositional symbol, and the other is entailment of CIs in the E LO dimension (to ensure that the DL and the propositional parts of the formula are satisfiable together). The next theorem formalises these results.
Theorem 2. The E LO formula satisfiability problem on partial interpretations is NP-complete and the entailment problem is PTime-complete. 4
We discuss the expressive power of free DLs. In particular, we define a notion
of bisimulation for ALCO that we use to characterise the expressive power
of concepts relative to first-order formulas interpreted on partial interpretations.
First, we present the definitions of bisimulation for ALCO and ALCOu, which are
standard in the literature [
Let I and J be partial interpretations, and let NC [ NR [ NI be a signature. An ALCO -bisimulation between I and J is a non-empty relation Z I J such that, for every d 2 I and e 2 J with (d; e) 2 Z, every concept name or nominal X formulated within , and every role name r in : (atom) d 2 XI iff e 2 XJ ; (forth) if (d; d0) 2 rI then there is e0 2 J such that (e; e0) 2 rJ and (d0; e0) 2 Z; and (back ) if (e; e0) 2 rJ then there is d0 2 I such that (d; d0) 2 rI and (d0; e0) 2 Z. An ALCOu -bisimulation (between I and J ) is an ALCO -bisimulation that is total, meaning that I and J are the domain and range of the relation.
Given a DL language L, a signature , and pointed interpretations (I; d) and (J ; e), we write (I; d) L (J ; e) if there is an L -bisimulation Z between I and J such that (d; e) 2 Z, and we say that (I; d) is L -bisimilar to (J ; e), or that Z is an L -bisimulation between (I; d) and (J ; e). We now introduce a suitable notion of bisimulation for ALCO .
Definition 1 (ALCO Bisimulation). A relation Z I J is an ALCO -bisimulation between I and J iff it is an ALCO -bisimulation between I and J that satisfies, in addition, the following conditions, for every (d; e) 2 Z: -bisimilar. (b) ALCO -bisimilar ( :1) there exists d0 2 I such that d 6= d0 and (I; d) ALCO (I; d0) iff there exists e0 2 J such that e0 6= e and (J ; e) ALCO (J ; e0); ( :2) if there is no d0 2 I such that d 6= d0 and (I; d) ALCO (I; d0), then for every u 2 I there exists v 2 J such that (u; v) 2 Z; ( :3) if there is no e0 2 J such that e 6= e0 and (J ; e) ALCO (J ; e0), then for every v 2 J there exists u 2 I such that (u; v) 2 Z.
Intuitively, Condition ( :1) says that, for two ALCO -bisimilar elements d and e, d has a distinct ALCO -bisimilar object (representing an ALCO -indistinguishable element in the same interpretation) iff e has one as well. Moreover, Condition ( :2) (respectively, ( :3)) states that if there is no distinct ALCO -bisimilar object to d 2 I (respectively, e 2 J ), then the ALCO -bisimulation relation is left-total (respectively, right-total ), that is, I (respectively, J ) is the domain (respectively, range) of the relation.
The next theorem states that ALCO -bisimilar elements satisfy the same
ALCO concepts C formulated within on partial interpretations (given a DL
language L, a signature , and pointed interpretations (I; d) and (J ; e), we
write (I; d) L (J ; e) iff it holds that d 2 CI iff e 2 CJ , for every L concept C
with C ). Moreover, under the assumption that the partial interpretations
satisfy the conditions of the class of !-saturated interpretations [
Theorem 3. For all signatures
and all partial interpretations I and J , (i) if (I; d) (ii) if (I; d)
ALCO (J ; e), then (I; d) ALCO (J ; e); ALCO (J ; e) and I; J are !-saturated, then (I; d) ALCO (J ; e).
Clearly, ALCOu and ALCO are both more expressive than ALCO. We now comment on the expressivity of ALCOu and ALCO . As illustrated in Figure 1, there are pointed interpretations (I; d) and (J ; e) that are ALCOu bisimilar but not ALCO -bisimilar, and, ALCO -bisimilar but not ALCOu -bisimilar, where A 2 . Since ALCOu and ALCO are invariant under their respective notions of bisimulation, it follows that the expressivity of concept expressions in these languages is not comparable. There is no ALCOu concept D equivalent to f Ag and no ALCO concept D equivalent to 8u:A. Proposition 1. The expressive power of ALCOu and ALCO comparable on partial (and on total) interpretations. concepts is not
We now characterise ALCO as the fragment of first-order logic on partial interpretations that is invariant under ALCO bisimulations. The standard translation of an ALCO concept C into a first-order formula x(C) (with at most one free variable x) is defined as usual for concepts built using ALCO constructors. For nominals of the form f Cg we have:
x(f Cg) = 9x x(C) ^ 8x8y( x(C) ^ y(C) ! x = y) ^ 8y( y(C) ! x = y): We say that a first-order formula '(x) with free variable x and such that ' is invariant under ALCO iff, for every (I; d) and (J ; e) such that (I; d) ALCO (J ; e), we have I; [x 7! d] j= '(x) iff J ; [x 7! e] j= '(x) (where [x 7! d] stands for any variable assignment that maps x to d).
Theorem 4. Let '(x) be a first-order formula with one free variable x and such that '(x) . The following conditions are equivalent: (i) there is an ALCO concept C such that x(C) is equivalent to '(x); (ii) '(x) is invariant under ALCO .
We leave open the question of which notion can precisely capture E LO . This notion should be less strict than ALCO bisimulations. One of the difficulties in finding it is that with f Cg one can express a limited form of disjunction. 5
The DLs proposed in this article introduce a mild form of cardinality constraints,
a set of constructors that has a long tradition in DL research [
In computational linguistics, the referring expression generation (REG )
problem is concerned with the (automatic) production of such noun phrases, so that
they can be used to describe an entity in a given domain [
Referring expressions are also relevant to other knowledge representation
tasks, as in the case of identity resolution problems [
Closely related are also the computation of explicit definitions of concepts
and the Beth definability property (BDP ) in DLs [
Finally, to the best of our knowledge, hybrid logics with non-denoting
nominals have not received much attention in the literature, with the exception of [