Skip to main content

A Proof-Theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in \(\cal EL\) w.r.t. Hybrid TBoxes

  • Conference paper
Logics in Artificial Intelligence (JELIA 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5293))

Included in the following conference series:

Abstract

Hybrid \(\cal EL\)-TBoxes combine general concept inclusions (GCIs), which are interpreted with descriptive semantics, with cyclic concept definitions, which are interpreted with greatest fixpoint (gfp) semantics. We introduce a proof-theoretic approach that yields a polynomial-time decision procedure for subsumption, and present a proof-theoretic computation of least common subsumers in \(\cal EL\) w.r.t. hybrid TBoxes.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ashburner, M., Ball, C.A., Blake, J.A., Botstein, D., Butler, H., Cherry, J.M., Davis, A.P., Dolinski, K., Dwight, S.S., Eppig, J.T., Harris, M.A., Hill, D.P., Issel-Tarver, L., Kasarskis, A., Lewis, S., Matese, J.C., Richardson, J.E., Ringwald, M., Rubin, G.M., Sherlock, G.: Gene ontology: tool for the unification of biology. Nat Genet. 25(1), 25–29 (2000)

    Article  Google Scholar 

  2. Baader, F.: Least common subsumers and most specific concepts in a description logic with existential restrictions and terminological cycles. In: Proc. IJCAI 2003. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  3. Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proc. IJCAI 2003. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  4. Baader, F., Brandt, S., Lutz, C.: Pushing the \(\mathcal{EL}\) envelope. In: Proc. IJCAI 2005. Morgan Kaufmann, San Francisco (2005)

    Google Scholar 

  5. Baader, F., Küsters, R., Molitor, R.: Computing least common subsumers in description logics with existential restrictions. In: Proc. IJCAI 1999. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  6. Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else? In: Proc. ECAI 2004. IOS Press, Amsterdam (2004)

    Google Scholar 

  7. Brandt, S.: Standard and Non-standard reasoning in Description Logics. Ph.D. dissertation, Institute for Theoretical Computer Science, TU Dresden, Germany (2006)

    Google Scholar 

  8. Brandt, S., Model, J.: Subsumption in \(\mathcal{EL}\) w.r.t. hybrid TBoxes. In: Furbach, U. (ed.) KI 2005. LNCS (LNAI), vol. 3698. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Hofmann, M.: Proof-theoretic approach to description-logic. In: Proc. LICS 2005. IEEE Press, Los Alamitos (2005)

    Google Scholar 

  10. Model, J.: Subsumtion in \(\mathcal{EL}\) bezüglich hybrider TBoxen. Diploma thesis, Institute for Theoretical Computer Science, TU Dresden, Germany (2005)

    Google Scholar 

  11. Novakovic, N.: Proof-theoretic approach to subsumption and least common subsumer in \(\mathcal{EL}\) w.r.t. hybrid TBoxes. Master thesis, Institute for Theoretical Computer Science, TU Dresden, Germany (2007)

    Google Scholar 

  12. Rector, A., Horrocks, I.: Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions. In: Proc. AAAI 1997. AAAI Press, Menlo Park (1997)

    Google Scholar 

  13. Baader, F.: Computing the least common subsumer in the description logic \(\cal EL\) w.r.t. terminological cycles with descriptive semantics. In: Ganter, B., de Moor, A., Lex, W. (eds.) ICCS 2003. LNCS, vol. 2746, pp. 117–130. Springer, Heidelberg (2003)

    Google Scholar 

  14. Spackman, K.: Managing clinical terminology hierarchies using algorithmic calculation: Experience with SNOMED-RT. Journal of the American Medical Informatics Association (2000); Fall Symposium Special Issue

    Google Scholar 

  15. Baader, F., Novakovic, N., Suntisrivaraporn, B.: A Proof-Theoretic Subsumption Reasoner for Hybrid \(\mathcal{EL}\)-TBoxes. In: Proceedings of the 2008 International Workshop on Description Logics (DL 2008). CEUR-WS (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Novaković, N. (2008). A Proof-Theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in \(\cal EL\) w.r.t. Hybrid TBoxes. In: Hölldobler, S., Lutz, C., Wansing, H. (eds) Logics in Artificial Intelligence. JELIA 2008. Lecture Notes in Computer Science(), vol 5293. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87803-2_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87803-2_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87802-5

  • Online ISBN: 978-3-540-87803-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics