We investigate the extension of description logics (DLs) with definite descriptions-that is, references to individuals based on descriptions of their properties. Specifically, we introduce the syntax and semantics for -individuals, modelled on the -terms that Hilbert introduced for first-order logic. We present sound and complete reasoning algorithms for the logics that result from adding -individuals to several well-known DLs. In particular, for the extension of the basic DL ℒ with -individuals, we provide a tableau calculus and show that the language without TBoxes is as expressive as the language with TBoxes; both also share EXPTIME-completeness of reasoning. In the case of the extension ℒ of the language with nominals, we give a reduction to the language ℒ with the universal role and show that reasoning remains EXPTIME-complete. Finally, for the lightweight DL ℰℒ, we show that the usual saturation calculus can be extended for -individuals, while maintaining the PTIME complexity.
In semantic modelling, it is often desirable to have a way to refer to individuals by describing their
properties. For example, one might want a way of referring to ‘the king of France’ based on a
formalisation of the ‘king of’ relation and the country of France. In engineering, a notation referring to
‘the temperature sensor on the exhaust pipe of the generator. . . ’ would be similar to tagging systems
commonly used in the engineering of industrial plants. Such references to individuals based on their
properties are known as definite descriptions , and they have been extensively studied in both logic and
philosophy [
The best known formalisation of definite descriptions is probably the one for first-order logic as
introduced by Hilbert [
In the context of description logics (DLs), Artale et al. [
While Artale et al. have demonstrated the viability of incorporating definite descriptions into DLs,
we believe that adopting the free logic approach to semantics is a significant departure from the
conventional DL framework. Hähnle [
Our results can be summarised as follows. After having formulated -individuals in the context of ℒ (Section 2), we provde a tableau calculus for this extension and show that the result of adding -individuals to the language without TBoxes renders it as expressive as the language with TBoxes; EXPTIME-completeness of reasoning is also preserved (Section 3). For the extension ℒ of ℒ with nominals, we present a reduction of the language with -individuals to one with the universal role, ℒ, thereby showing that reasoning remains in EXPTIME (Section 4). Finally, for the lightweight DL ℰ ℒ, we show that the usual saturation calculus can be extended to support -individuals, while preserving PTIME completeness of concept subsumption (Section 5).
Full proofs of all claims in this paper can be found in the technical report [
We begin with the syntax of ℒ extended with -individuals, which we call ℒ. We first do this for concepts and individuals, where the latter includes -individuals . as a new syntactic category, which can be added not only to ℒ but also to any DL. These individuals may be used wherever an individual name is allowed, which, in the case of ℒ, means only in ABox assertions. However, we will later consider logics ℒ and ℰ ℒ with nominals, where -individuals may also appear in concept descriptions.
Definition 1 (ℒ Syntax). Let , , and be sets of concept names, role names, and individual names, respectively. Then, ℒ concepts and individual descriptions, and , are defined by the following grammar: ::= | ¬ | ⊓ | ⊔ | ∃. | ∀., ::= | ., where , , and range over , , and , respectively. An assertional axiom is an expression of the form ( ) or ( 1, 2) where is a concept, a role name, and , 1, 2 individual descriptions. An ℒ concept inclusion axiom is of the form ⊑ for concepts and . Then, ℒ ABox and TBox are sets of ℒ assertional and concept inclusion axioms, respectively. An ℒ knowledge base ( KB) is a pair = (, ) consisting of an ABox and a TBox .
Note that all ℒ concepts are also in plain ℒ, and the same holds for TBoxes.
We now move on to the semantics, beginning with the definition of interpretations for concepts
and individual descriptions. For later discussion, it is convenient to first define interpretations that
impose no restrictions on the interpretation of an individual ., apart from the requirement that all
syntactically identical occurrences be interpreted the same, as stated in property (iii) in the introduction.
We then constrain interpretations to satisfy the central intended property of -individuals—property
(ii) in the introduction. It is common in the literature on -terms (e.g. [
Definition 2 (Interpretations and Intentional Interpretations). An interpretation is a pair ℐ = (∆ ℐ , · ℐ ), where domain ∆ ℐ is a non-empty set, and · ℐ is a function mapping each concept name to ℐ ⊆ ∆ ℐ , each role name to ℐ ⊆ ∆ ℐ × ∆ ℐ , and each individual description to ℐ ∈ ∆ ℐ . Then, for each ℒ concepts , and role name , let ( ⊓ )ℐ = ℐ ∩ ℐ , ( ⊔ )ℐ = ℐ ∪ ℐ , (¬)ℐ = ∆ ℐ ∖ ℐ , (∃.)ℐ = { ∈ ∆ ℐ | there exists ⟨, ⟩ ∈ ℐ such that ∈ ℐ }, (∀.)ℐ = { ∈ ∆ ℐ | for all ⟨, ⟩ ∈ ℐ , ∈ ℐ }.
An interpretation ℐ is intensional if (.)ℐ ∈ ℐ for each concept such that ℐ ̸= ∅,.
We emphasise that -individuals based on semantically equivalent concepts may not be interpreted the same; for instance, there is no guarantee that (.( ⊓))ℐ = (.( ⊓))ℐ . An alternative approach would be to define the semantics of . as a function of the extension ℐ . The properties of such semantics, usually referred to as extensional, are left as future work.
We also note that the definition imposes no restriction on .ℐ when ℐ = ∅. In this case, the value may be any domain element, potentially diferent ones for syntactically diferent concept descriptions, but still committed to be the same one for all syntactically identical .
We move on to the semantics of ℒ KBs.
Definition 3 (Semantics of Axioms and Knowledge Bases). Given an ℒ axiom and interpretation ℐ, the satisfaction of , written ℐ |= , is defined, for diferent forms of , as follows: ℐ |= ( ) if ℐ ∈ ℐ , ℐ |= ( 1, 2) if ⟨ 1ℐ , 2ℐ ⟩ ∈ ℐ , ℐ |= ⊑ if ℐ ⊆ ℐ .
Then, ℐ satisfies a KB = (, ), written ℐ |= , if it satisfies each axiom in and in . A KB is satisfiable if there exists an interpretation ℐ that satisfies . It is intensionally satisfiable if there exists such an intensional interpretation.
The extension of the language by intensionally interpreted -individuals is conservative, in the sense that every ‘standard’ interpretation can be extended to an intensional one.
the form .. Then, is satisfiable if and only if is intensionally satisfiable.
Proof. The backward direction follows from the definition. For the forward direction, assume that is satisfiable and let ℐ |= . Let : (∆ ℐ ) → ∆ ℐ be a choice function—that is, a function that selects an element in the argument subset of ∆ ℐ if this subset is non-empty and an arbitrary element of ∆ ℐ otherwise. Let an intentional interpretation ℐ have domain ∆ ℐ , interpret all concept, role, and individual names as ℐ, and have .ℐ = (ℐ ) for each .
An initial observation regarding reasoning in ℒ is that -individuals in ABox axioms of the form (.) can be used to express arbitrary TBox axioms: for each concept , we have ℐ |= (¬)(.) if and only if ℐ = ∅, and thus, for every two concept descriptions and , ℐ |= ⊑ ⇐⇒ ( ⊓ ¬)ℐ = ∅ ⇐⇒ ℐ |= (¬ ⊔ )(( ⊓ ¬)).
(1)
This equivalence immediately yields a lower bound on expressive power (and as a result, eficiency
of reasoning): ℒ under intensional semantics without TBoxes is at least as expressive as ℒ
with general TBoxes. Thus, ℒ ABox satisfiability is EXPTIME-hard [
Before this, however, we introduce a tableau calculus for the satisfiability problem in ℒ, focusing on ABox; in light of equivalence (1), this calculus applies also to ℒ KBs. Our calculus operates concepts in negation normal form—that is, with negation applied only to concept names. Reasoning about -individuals . requires distinguishing two cases: one where ℐ is non-empty, in which case ℐ |= (.), and one where ℐ is empty. The latter is expressible as (¬)(.), but this introduces an additional negation that disrupts the negation normal form and thus requires re-normalisation. This, in turn, complicates the reasoning process when saturating open branches. So, we instead introduce a new auxiliary form of ABox axioms, , which expresses the emptiness of a concept . However, we emphasise that such axioms are introduced purely as a reasoning aid, as is semantically equivalent to (¬)(.).
We are now ready to define the negation normal form.
Definition 6 (Negation Normal Form). An ℒ concept is in negation normal form ( NNF) if negation appears only in front of concept names. A Ξ -ABox is in NNF if, for every axiom of the form ( ) in , the concept is in NNF.
As usual, every concept and, thus every Ξ -ABox can be transformed in polynomial time into an equivalent concept and ABox, respectively, in NNF, which are denoted ∼ and ∼ .
Note that we do not require the concepts within -individuals in an ABox in NNF to be in NNF. In fact, such transformations must be avoided, as they may alter the syntactic identity of individual descriptions. For instance, if 1 and 2 are syntactically diferent, then .1 and .2 may be interpreted diferently, but if their respective NNFs ∼ 1 and ∼ 2 are syntactically identical, then .(∼ 1) and .(∼ 2) must be interpreted by the same domain element. Moreover, the concept in a Ξ -axiom need not be in NNF, even if the containing ABox is.
The tableau calculus for ℒ, which is defined next, is based on the one by Bucheit et al. [
certain individual descriptions are designated to be ancestors of others, a rule application replaces some ABox in by one or two ABoxes ′ and (potentially) ′′ (where the ancestry relation for common individual descriptions is inherited from ) by the following rules: 1. if includes (1 ⊓ 2)( ), but not both 1( ) and 2( ), then ′ := ∪ {1( ), 2( )}; 2. if includes (1 ⊔ 2)( ), but neither 1( ) nor 2( ), then ′ := ∪ {1( )} and ′′ := ∪ {2( )}; 3. if includes (∀.)( ) and (, ′), but not ( ′) then ′ := ∪ {( ′)}; 4. if includes (∃.)( ) such that there is no ′ with ( ′) and (, ′) in , and there is no ancestor ′′ of that is blocked—that is, has an ancestor ′′′ such that ′( ′′) ∈ implies ′( ′′′) ∈ for every concept ′—then ′ := ∪ {(), (, )}, where is a fresh individual name with ancestors and all ancestors of (assuming that is suficiently large); 5. if includes 1(.2), but neither (∼ 2)(.2) nor 2, then ′ := ∪ {(∼ 2)(.2)} and ′′ := ∪ {2}; 6. if includes and an individual description is mentioned in an axiom in , but (∼ (¬))( ) is not in , then ′ := ∪ {(∼ (¬))( )}.
Among the rules in Definition 7, the first four are inherited from the standard tableau calculus for ℒ, while the last two address reasoning with -individuals. In particular, Rule 5 splits the branch into two: if an ABox includes some ., then either . satisfies or is empty. Then, Rule 6 is essentially a reframing of the standard TBox-rule in terms of Ξ -axioms.
We argue the correctness of our calculus by means of soundness and completeness theorems. Theorem 8 (Soundness). Let ′ be a set of Ξ -ABoxes obtained from a set of Ξ -ABoxes in NNF by an application of a rule in Definition 7. Then, each ABox in ′ is in NNF. Moreover, if each ABox in ′ is intensionally unsatisfiable, then each ABox in is intensionally unsatisfiable.
Proof sketch. Let ′ and (potentially) ′′ be the Ξ -ABoxes obtained by a rule application to a Ξ -ABox . We show that if is intensionally satisfiable, then either ′ or ′′ is intensionally satisfiable. We concentrate on Rules 5 and 6 here, since the other rules are standard.
Assume first that Rule 5 is applied to 1(.2) and ℐ is an intensional interpretation such that ℐ |= 1(.2). If 2ℐ ̸= ∅ then (.2)ℐ ∈ 2ℐ since ℐ is intensional, and so ℐ |= 2(.2), implying ℐ |= (∼ 2)(.2). Otherwise, ℐ |= 2 by definition.
Assume now that Rule 6 is applied to . By definition, ℐ = ∅, and so /∈ ℐ implies ∈ (¬)ℐ = (∼ (¬))ℐ for every individual description .
Theorem 9 (Completeness). Assume that no rules in Definition 7 is applicable to a set of Ξ -ABoxes in NNF. If ∈ contains no clash then is intensionally satisfiable.
Proof sketch. Given an ABox as described, we construct an intentional interpretation ℐ satisfying . The domain ∆ ℐ of ℐ consist of all individual descriptions mentioned in . Then, for each individual description appearing in , we set ℐ = ; in particular, for every concept , if . appears in then (.)ℐ = .. Moreover, for . not mentioned in , we set (.)ℐ = (ℐ ) for a choice function for ∆ ℐ . Finally, for each concept name , we set ℐ = { | ( ) ∈ }, and for each role name , we define ℐ as follows: if ( 1, 2) ∈ , then ⟨ 1, 2⟩ ∈ ℐ , and if 1 is blocked by 1′ and ( 1′ , 2) ∈ , then ⟨ 1, 2⟩ ∈ ℐ . It is a routine to show that ℐ is intentional and satisfies .
Theorems 8 and 9 give us the following result; note that termination follows from the same arguments
as for plain ℒ (with TBox) [
terminates on {∼} after a finite number of rule applications. Moreover, is satisfiable if and only if the set of ABoxes after the termination contains an ABox without a clash.
We finish the section with the complexity of ℒ reasoning.
As mentioned above, the lower bound follows from the facts that we can encode TBoxes in ℒ
ABoxes and that ℒ concept satisfiability with TBox is EXPTIME-complete [
extending Definition 1 with concepts of the form { }, called nominals, with an individual description.
For example, .({.} ⊔ {.}) is an ℒ individual description with nested -individuals. Definition 13 (Semantics of ℒ). Interpretations ℐ = (∆ ℐ , · ℐ ) for ℒ extend Definition 2 by interpreting { }ℐ = { ℐ } for every individual description . Intensionality, satisfaction, and ( intentional) satisfiability then applies to ℒ as in Definitions 2 and 3.
Although we do not adopt the UNA, we can express 1 ̸= 2 in ℒ as { 1} ⊓ { 2} ⊑ ⊥.
As said above, we next reduce ℒ reasoning to reasoning in the standard DL ℒ. Formally, it is the same as ℒ except that it does not allow for -individuals, but uses extended with a special role that is interpreted as ∆ ℐ × ∆ ℐ in every interpretation ℐ.
every -individual . mentioned in , the ABox axiom (¬∃. ⊔ )(.), and then replacing, in each axiom (including the ones added at the first step), every occurrence of an -individual . that is not part of another -individual with .
We now show that this reduction indeed preserves the satisfiability of KBs. The key part of the proof is the iterative construction of an ℒ intentional interpretation from an ℒ interpretation. This construction is not trivial as it must guarantee the intensionality not only for the -individuals occurring in the KB, but for all such individuals.
Proof sketch. Let be a ℒ KB and * be its ℒ reduction.
For the forward direction, assume that ℐ |= for an intentional interpretation ℐ. Define the ℒ-interpretation ℐ* with ∆ ℐ* = ∆ ℐ as follows. For each concept, role, or individual name in the language of , set ℐ* = ℐ , and for each obtained from the corresponding ., set ℐ* = .ℐ . It follows immediately from the definitions that ℐ = (* )ℐ* for every concept appearing in and its corresponding replacement * as in Definition 14, and hence all axioms in * that are reductions of the axioms in are satisfied by ℐ* . Moreover, the reductions of the added axioms (¬∃. ⊔ )(.) are also satisfied, which can be shown by simple analysis of two cases: whether (* )ℐ* is empty or not.
For the backward direction, let ℐ* |= * for an interpretation ℐ* . We construct an ℒinterpretation ℐ as the limit of interpretations, each handling subsequent ‘layers’ of -nesting. To this end, we first let 0 be the union of , , , and the set of all . such that contains no individual descriptions, and then, for each ≥ 0, let +1 be the set of all . such that mentions at least one individual description from and all individual descriptions mentioned in it are from 1, . . . , . Using these sets, we next construct a sequence of interpretations ℐ, ≥ 0. First, we let ℐ0 be defined as follows: ∆ ℐ0 = ∆ ℐ* ; then for each concept, role, and individual name , we let ℐ0 = ℐ* ; then, for each . ∈ 0, if appears in * , then we set .ℐ0 = ℐ* , and otherwise we set .ℐ0 = (ℐ* ), where is a choice function; finally, for every other ., we set .ℐ0 = for an arbitrary ∈ ∆ ℐ0 (note that, for ℐ, the latter will be all redefined later). Then, for each ≥ 0, we define ℐ+1 as follows: ∆ ℐ+1 = ∆ ℐ ; for each . ∈ +1, if appears in * , then we set .ℐ+1 = ℐ* , and otherwise, we set .ℐ+1 = (ℐ ), where is again a choice function; finally, for every other concept, role name, or individual description , we set ℐ+1 = ℐ . We now define ℐ = ⋃︀≥ 0 ℐ′, where, for each ≥ 0, ℐ′ is the restriction of ℐ to ⋃︀=0 . We can then show that ℐ is indeed an intentional interpretation of .
To conclude this section, we argue the complexity of reasoning in ℒ.
Proof. The lower bound is argued in Theorem 11. For the upper bound, we can first observe that the
reduction in Definition 14 can be realised in polynomial time, then apply Theorem 15 to reduce our
problem to satisfiability of ℒ KBs, and finally apply the observation of Artale et al. [
In this section, we study the impact of adding -individuals to the lightweight DL ℰ ℒ. As with plain ℰ ℒ, satisfiability in the extended logic ℰ ℒ is trivial, since all KBs are satisfiable. Thus, in line with standard practice for ℰ ℒ-based DLs, our reasoning problem is concept subsumption—that is, the problem of checking whether a KB entails, over intentional interpretations, an inclusion axiom 1 ⊑ 2. We will write this entailment as |= 1 ⊑ 2. We show that concept subsumption ℰ ℒ can be reduced to the case where has empty ABox and all inclusion axioms (including 1 ⊑ 2) are in a simple normal form. We then extend the standard ℰ ℒ concept subsumption algorithm to handle ℰ ℒ in this form. Before proceeding, we note that adding -individuals to a more standard DL ℰ ℒ is not very interesting, as concept subsumption in the resulting logic coincides with concept subsumption in plain ℰ ℒ.
::= | ⊓ | ∃. | { } | ⊤.
The semantics of ℰ ℒ is inherited from ℒ, with ⊤ℐ = ∆ ℐ for every interpretation ℐ.
We next define the normal form for ℰ ℒ KBs, which has no ABox and no complex concepts. Definition 18 (Normal Form). An ℰ ℒ KB is in normal form if its ABox is empty and inclusion axioms are of the following forms, where each , 1, 2, is ⊤, a concept name, or a nominal { }, for an individual name or an -individual . with a concept name : ⊑ , 1 ⊓ 2 ⊑ , ⊑ ∃., ∃. ⊑ .
We next show that each ℰ ℒ KB can be easily normalised.
form such that, for every axiom in the signature of , |= if and only if ′ |= . Proof sketch. Given an ℰ ℒ KB we can first eliminate complex concepts in -individuals by replacing each . in that is not nested within another -individual with . , for a fresh concept name, and adding the corresponding axiom ≡ (as usual, expressible using concept inclusions). Then, we can apply usual normalisation as for ℰ ℒ.
The following procedure takes as input an ℰ ℒ KB in normal form and concept names , . This procedure determines whether |= ⊑ . Note that the procedure can be generalised to checking whether |= ⊑ for arbitrary concepts , by applying the algorithm to the normalisation of ∪ { ≡ , ≡ }, where , are fresh concept names.
Definition 20 (Entailment Procedure for ℰ ℒ). Let be an ℰ ℒ KB in normal form and , be concept names. For each concept and role name mentioned in , initialise the following sets of concepts and pairs of concepts, respectively: () = {, ⊤} and () = ∅. Update these sets according to the following rules until no rules can be applied, where the relation ⇝ on concept pairs is defined so that ⇝ if and only if there exist concepts 1, . . . , such that 1 = or 1 = { } for some individual description , ( , +1) ∈ ( ) for some role name for each = 1, . . . , − 1, and = : (CR1) if ′ ∈ (), ′ ⊑ ∈ , and ∈/ (), then set () := () ∪ {}; (CR2) if 1, 2 ∈ (), 1 ⊓ 2 ⊑ ∈ , and ∈/ (), then set () := () ∪ {}; (CR3) if ′ ∈ (), ′ ⊑ ∃. ∈ , and (, ) ∈/ (), then set () := () ∪ {(, )}; (CR4) if (, )∈(), ′ ∈ (), ∃.′ ⊑ ∈ , and ∈/ (), then set () := ()∪{}; (CR5) if {} ∈ () ∩ (), ⇝ and () ̸⊆ (), then set () := () ∪ (); (CR6) if ⇝ and ∈/ ({.}), then set ({.}) := ({.}) ∪ {}.
Output yes if and only if ∈ ().
The correctness of the algorithm follows from the soundness and completeness theorems.
an intensional interpretation such that ℐ |= and ℐ ̸= ∅. The following conditions are satisfied by the initial sets () and () for each two concepts , ′, and role in the procedure in Definition 20 applied to , , and : (I1) ′ ∈ () =⇒ ℐ |= ⊑ ′, (I2) (, ′) ∈ () =⇒ ℐ |= ⊑ ∃.′.
Moreover, if these conditions are satisfied before the application of a rule, then they are satisfied after this application.
Proof sketch. For the initial sets, both conditions hold by construction.
Let now and be the sets before the application of a rule. In this sketch, we concentrate only on the rules relevant to the -individuals: (CR5) and (CR6). Since the sets only expand, we only need to show that the conditions are satisfied for the added elements (which means, in particular, that in this sketch we concern only about (I1)).
Let the rule be (CR5). Since ⇝ , there are 1, . . . , such that 1 = or 1 = { }, = , and ( , +1) ∈ ( ) for some for each . Since ℐ ̸= ∅ and, by definition, { }ℐ ̸= ∅, we have 1ℐ ̸= ∅. Thus, by definition of ⇝ and condition (I2), ℐ ̸= ∅. Since, ℐ ⊆ { ℐ } and ℐ ⊆ { ℐ } by (I1), we conclude that ℐ ⊆ { }ℐ = ℐ . As such, if some ′ is in () (and thus in () after the rule application), we have ℐ ⊆ ℐ ⊆ (′)ℐ as needed.
Let the rule be (CR6). As for (CR5), ℐ ̸= ∅. Since ℐ is intensional, we have .ℐ ∈ ℐ .
be sets of concepts and pairs of concepts, obtained by the procedure in Definition 20 applied to , , and so that no further rules can be applied. Then, |= ⊑ implies ∈ ().
Proof. Let |= ⊑ , but assume that ∈/ (). We will construct an intensional interpretation ℐ such that ℐ |= , but ℐ ̸⊆ ℐ .
Let ∼ ′ for concepts and ′ if and only if = ′ or there is some {} ∈ () ∩ (′). The inapplicability of rule (CR6) implies that ∼ is an equivalence relation. Moreover, for each , ′, such that ∼ ′ and for each ∈ , we have () = (′) and (, ) ∈ () implying (′, ) ∈ (). Indeed, the former follows from the inapplicability of rule (CR5). For the latter, note that there must be some iteration of the procedure where (, ) is added to () by rule (CR3). Thus, there is some 1 ∈ () with 1 ⊑ ∃. ∈ . By the former, () = (′), and so 1 ∈ (′). Thus, (′, ) ∈ () since rule (CR3) is not applicable.
We are now ready to construct ℐ. First we set ∆ ℐ to be the set of all equivalence classes [] over ∼ for concepts such that ⇝ . Then, we set (′)ℐ = {[] | ′ ∈ ()} for each concept name ′ such that ⇝ ′ and (′)ℐ = ∅ for each other concept name ′. Moreover, we set ℐ = {⟨[], []⟩ | (, ) ∈ ()} for each role name . Finally, we set ℐ = [{ }] for each individual description with ⇝ { }, and, for other individual descriptions , ℐ = [] if is an individual name and ℐ = ((′)ℐ ) for a choice function on ∆ ℐ if = .′ (recall that (∅) is an arbitrary element by definition of a choice function).
Interpretation ℐ is intensional: for each concept name ′ with (′)ℐ ̸= ∅, if ⇝ {.(′)}, (.(′))ℐ ∈ (′)ℐ since (CR6) is inapplicable, and otherwise .ℐ = (ℐ ) ∈ ℐ .
The rest of the proof is mostly a result of the following claim.
Claim 23. For each [] ∈ ∆ ℐ and as in Definition 18, [] ∈ ℐ if and only if ∈ (). Proof. Consider each possible form of . If = ⊤ then the claim follows since ⊤ ∈ (). If is a concept name, then it follows by construction of ℐ . Finally, let = { }. On the one hand, [] ∈ { }ℐ implies ℐ = [], [] = [{ }] by definition of ℐ , and, since { } is in ({ }) initially and [{ }] ∼ , we have { } ∈ (). On the other hand, if { } ∈ (), we have [] = [{ }] by definition of ∼ , and so ℐ = [], implying [] ∈ { }ℐ .
In order to show that ℐ ̸⊆ ℐ , we observe that [] ∈ ℐ by construction, but, by Claim 23, [] ∈/ ℐ , since ∈/ ().
We are left to show that ℐ |= . To this end, consider each form of an axiom in .
Let ⊑ . For every ′ with [′] ∈ ℐ , we have ∈ (′) by Claim 23. Since rule (CR1) is inapplicable, ∈ (′), and so [′] ∈ ℐ also by Claim 23.
Let ⊑ 1 ⊓ 2. This case is similar to the previous one, except that we use rule (CR2).
Let ⊑ ∃.. For each ′ with [′] ∈ ℐ , ∈ (′) by Claim 23. Since rule (CR3) is inapplicable, (′, ) ∈ (). Then, ⟨[′], ⟩ ∈ ℐ implies [] ∈ ℐ and so [′] ∈ (∃.)ℐ .
Let ∃. ⊑ . For each ′ with [′] ∈ (∃.)ℐ , there exists some [′] ∈ ∆ ℐ such that ⟨[′], [′]⟩ ∈ ℐ and [′] ∈ ℐ . Thus, there is some ′′ ∈ [′] such that (′, ′′) ∈ (). Since [′′] = [′] ∈ ℐ , we have ∈ (′′) by Claim 23, and so ∈ (′) since rule (CR4) is inapplicable. Finally, Claim 23 gives us [′] ∈ ℐ , as needed.
procedure of Definition 20 terminates. Moreover, |= ⊑ if and only it answers yes. Proof. First, observe that the procedure is always terminating, because both and are subsets of finite sets and every rule increases one such set; nothing is ever removed. The soundness and completeness follow from Theorems 21 and 22.
Finally, we show that the complexity of concept subsumption in ℰ ℒ is the same as in ℰ ℒ.
Proof. The lower bound is inherited from ℰ ℒ, for which it follows from the PTIME-completeness of satisfiability of propositional Horn clauses [ 21]. The upper bound is by Proposition 19 and since the procedure in Definition 20 is polynomial, because no rules remove any elements from the sets and there only polynomial number of possible elements in total.
In this paper, we studied the efect of adding Hilbert-style -individuals with intensional semantics to the description logics ℒ, ℒ, and ℰ ℒ. We demonstrated that existing reasoning algorithms, including tableaux for ℒ satisfiability and TBox saturation for ℰ ℒ concept subsumption, can be extended to -individuals; however, the proofs of correctness of these algorithms—especially completeness—are far from trivial. In most cases (but not always), the complexity of reasoning is also preserved. For future work, we suggest studying the extensional semantics of -individuals in the context of DLs. The inclusion of reasoning about -individuals in other calculi for DL, such as hyper-tableaux [22], is also interesting.
During the preparation of this work, the authors used GPT-4 in order to grammar and spelling check. [19] M. J. Fischer, R. E. Ladner, Propositional dynamic logic of regular programs, J. Comput. Syst. Sci.
18 (1979) 194–211. [20] S. Passay, T. Tinchev, An essay in combinatory dynamic logic, Inf. Comput. 93 (1991) 263–332. [21] S. Cook, P. Nguyen, Logical foundations of proof complexity, Cambridge University Press, 2010. [22] B. Motik, R. Shearer, I. Horrocks, Hypertableau reasoning for description logics, J. Artif. Int. Res. 36 (2009) 165–228.