Skip to main content
SpringerLink
Log in

Optimized Reasoning in Description Logics Using Hypertableaux

  • Conference paper
Book cover Automated Deduction – CADE-21 (CADE 2007)

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

Included in the following conference series:

Abstract

We present a novel reasoning calculus for Description Logics (DLs)—knowledge representation formalisms with applications in areas such as the Semantic Web. In order to reduce the nondeterminism due to general inclusion axioms, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. To prevent the calculus from generating large models, we introduce “anywhere” pairwise blocking. Our preliminary implementation shows significant performance improvements on several well-known ontologies. To the best of our knowledge, our reasoner is currently the only one that can classify the original version of the GALEN terminology.

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

Access this chapter

Log in via an institution
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. Baader, F., Buchheit, M., Hollunder, B.: Cardinality Restrictions on Concepts. Artificial Intelligence 88(1-2), 195–213 (1996)

    Article  MATH  Google Scholar 

  2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F.: The Description Logic Handbook. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  3. Baumgartner, P., Furbach, U., Niemelä, I.: Hyper Tableaux. In: Orłowska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol. 1126, pp. 1–17. Springer, Heidelberg (1996)

    Google Scholar 

  4. Donini, F.M., Massacci, F.: EXPTIME tableaux for ALC. Artificial Intelligence 124(1), 87–138 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Fermüller, C., Tammet, T., Zamov, N., Leitsch, A.: Resolution Methods for the Decision Problem. LNCS, vol. 679. Springer, Heidelberg (1993)

    MATH  Google Scholar 

  6. Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution Decision Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, vol. II, pp. 1791–1849. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  7. Goré, R.P., Nguyen, L.: EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol. 4548, Springer, Heidelberg (2007)

    Google Scholar 

  8. Haarslev, V., Möller, R.: RACER System Description. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 701–706. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Horrocks, I., Sattler, U.: A Description Logic with Transitive and Inverse Roles and Role Hierarchies. Journal of Logic and Computation 9(3), 385–410 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  10. Horrocks, I., Sattler, U., Tobies, S.: Reasoning with Individuals for the Description Logic SHIQ. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 482–496. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Hudek, A.K., Weddell, G.: Binary Absorption in Tableaux-Based Reasoning for Description Logics. In: Proc. DL, Windermere, UK (May 30-June 1, 2006)

    Google Scholar 

  12. Hustadt, U., Motik, B., Sattler, U.: Data Complexity of Reasoning in Very Expressive Description Logics. In: Proc. IJCAI 2005, pp. 466–471, Edinburgh, UK (July 30-August 5, 2005)

    Google Scholar 

  13. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexity Boundaries for Horn Description Logics. In: Proc. AAAI 2007, Vancouver, BC, Canada, July 22-26, 2007, AAAI Press (to appear)

    Google Scholar 

  14. Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Universität Karlsruhe, Germany (2006)

    Google Scholar 

  15. Parsia, B., Sirin, E.: Pellet: An OWL-DL Reasoner. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds.) ISWC 2004. LNCS, vol. 3298, Springer, Heidelberg (2004)

    Google Scholar 

  16. Plaisted, D.A., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Logic and Computation 2(3), 293–304 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  17. Robinson, A.: Automatic Deduction with Hyper-Resolution. Int. Journal of Computer Mathematics 1, 227–234 (1965)

    MATH  Google Scholar 

  18. Schmidt, R.A., Hustadt, U.: A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In: Baader, F. (ed.) Automated Deduction – CADE-19. LNCS (LNAI), vol. 2741, pp. 412–426. Springer, Heidelberg (2003)

    Google Scholar 

  19. Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, Germany (2001)

    Google Scholar 

  20. Tsarkov, D., Horrocks, I.: Efficient Reasoning with Range and Domain Constraints. In: Proc. DL 2004, Whistler, BC, Canada (June 6-8, 2004)

    Google Scholar 

  21. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292–297. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, UK

    Boris Motik, Rob Shearer & Ian Horrocks

Authors
  1. Boris Motik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rob Shearer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ian Horrocks
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Motik, B., Shearer, R., Horrocks, I. (2007). Optimized Reasoning in Description Logics Using Hypertableaux. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73595-3_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73594-6

  • Online ISBN: 978-3-540-73595-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation