Number Restrictions on Transitive Roles in
         Description Logics with Nominals?

Vı́ctor Gutiérrez-Basulto1 , Yazmı́n Ibáñez-Garcı́a2 , and Jean Christoph Jung3
     Cardiff University, UK1   TU Wien, Austria2 Universität Bremen, Germany3

    One of the main applications of description logics (DLs) is the formalization
of ontologies from the biomedical domain, in which support for describing and
classifying certain terms depending on the number of components (in a transitive
sense) constituting them is often required, see e.g., [1]. Motivated by this type of
applications, the DL community has investigated various languages supporting
number restrictions on both transitive and non-transitive roles. Unfortunately,
the combination of these features with other classical DL constructs, such as
inverse roles or role inclusions, easily leads to undecidability [2]. On the positive
side, it was shown that extensions of ALC with these features (and nominals)
are decidable [2, 3]. However, no (elementary) complexity bounds were known.
    In this paper, we complete the picture of the complexity of the problem of
concept satisfiability relative to TBoxes in DLs supporting counting over transi-
tive roles. First, we establish a tight NExpTime upper bound for the DL SOQ.
To this aim, we provide a decomposition of SOQ models, allowing to ‘indepen-
dently reason’ about distinct roles. Then, based on a technique in [4], we show
a small (that is, exponential) model property of each member of the decomposi-
tion, leading to the desired upper bound. For SON , the restriction of SOQ to
unqualified number restrictions, we show that the coding of numbers has an im-
pact on the computational complexity: satisfiability is ExpTime-complete with
unary coding of numbers, and NExpTime-complete with binary one. For the
logics SHIF and SHOIF, allowing only for functionality, we show that satisfi-
ability is not harder than when counting only over non-transitive roles is allowed.
Finally, we initiate the study of DL-Lite with counting over transitive roles. We
show that satisfiability in the core fragment of DL-Lite with role inclusions is
undecidable, and provide complexity results for the case of functionality.

References
1. Wolstencroft, K., Brass, A., Horrocks, I., Lord, P., Sattler, U., Turi, D., Stevens, R.:
   A little semantic web goes a long way in biology. In: Proc. of ISWC-05. (2005)
2. Kazakov, Y., Sattler, U., Zolin, E.: How many legs do I have? non-simple roles in
   number restrictions revisited. In: Proc. of LPAR-07. (2007) 303–317
3. Kaminski, M., Smolka, G.: Terminating tableaux for SOQ with number restrictions
   on transitive roles. In: Proc. of the 6th IFIP TC. (2010) 213–228
4. Kazakov, Y., Pratt-Hartmann, I.: A note on the complexity of the satisfiability
   problem for graded modal logics. In: Proc. of LICS-09. (2009) 407–416

?
    Accepted at AAAI 2017. Gutiérrez-Basulto was funded by the EU’s Horizon 2020
    programme under the Marie Sklodowska-Curie grant No 663830.