<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Number Restrictions on Transitive Roles in Description Logics with Nominals?</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>V ctor Gutierrez-Basulto</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Yazm n Iban~ez-Garc a</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
          <xref ref-type="aff" rid="aff2">2</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Jean Christoph Jung</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Cardi University</institution>
          ,
          <country country="UK">UK</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>TU Wien</institution>
          ,
          <country country="AT">Austria</country>
        </aff>
        <aff id="aff2">
          <label>2</label>
          <institution>Universitat Bremen</institution>
          ,
          <country country="DE">Germany</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>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 satis ability relative to TBoxes in DLs supporting counting over transitive 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 `independently 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 decomposition, leading to the desired upper bound. For SON , the restriction of SOQ to unquali ed number restrictions, we show that the coding of numbers has an impact on the computational complexity: satis ability 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 satis 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 satis ability in the core fragment of DL-Lite with role inclusions is undecidable, and provide complexity results for the case of functionality.</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>Wolstencroft</surname>
            ,
            <given-names>K.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Brass</surname>
            ,
            <given-names>A.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Horrocks</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Lord</surname>
            ,
            <given-names>P.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sattler</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Turi</surname>
            ,
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Stevens</surname>
            ,
            <given-names>R.:</given-names>
          </string-name>
          <article-title>A little semantic web goes a long way in biology</article-title>
          .
          <source>In: Proc. of ISWC-05</source>
          . (
          <year>2005</year>
          )
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Kazakov</surname>
            ,
            <given-names>Y.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Sattler</surname>
            ,
            <given-names>U.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Zolin</surname>
          </string-name>
          , E.:
          <article-title>How many legs do I have? non-simple roles in number restrictions revisited</article-title>
          .
          <source>In: Proc. of LPAR-07</source>
          . (
          <year>2007</year>
          )
          <volume>303</volume>
          {
          <fpage>317</fpage>
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Kaminski</surname>
            ,
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Smolka</surname>
          </string-name>
          , G.:
          <article-title>Terminating tableaux for SOQ with number restrictions on transitive roles</article-title>
          .
          <source>In: Proc. of the 6th IFIP TC</source>
          . (
          <year>2010</year>
          )
          <volume>213</volume>
          {
          <fpage>228</fpage>
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Kazakov</surname>
            ,
            <given-names>Y.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Pratt-Hartmann</surname>
            ,
            <given-names>I.</given-names>
          </string-name>
          :
          <article-title>A note on the complexity of the satis ability problem for graded modal logics</article-title>
          .
          <source>In: Proc. of LICS-09</source>
          . (
          <year>2009</year>
          )
          <volume>407</volume>
          {
          <fpage>416</fpage>
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>