Skip to main content
SpringerLink
Log in

Resolution-Based Reasoning for Ontologies

  • Chapter
  • First Online:
Book cover Handbook on Ontologies

Part of the book series: International Handbooks on Information Systems ((INFOSYS))

Summary

We overview the algorithms for reasoning with description logic (DL) ontologies based on resolution. These algorithms often have worst-case optimal complexity, and, by relying on vast experience in building resolution theorem provers, they can be implemented efficiently. Furthermore, we present a resolution-based algorithm that reduces a DL knowledge base into a disjunctive datalog program, while preserving the set of entailed facts. This reduction enables the application of optimization techniques from deductive databases, such as magic sets, to reasoning in DLs. This approach has proven itself in practice on ontologies with relatively small and simple TBoxes, but large ABoxes.

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 349.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 449.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 449.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    http://kaon2.semanticweb.org/

References

  1. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison Wesley, 1995.

    Google Scholar 

  2. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, January 2003.

    Google Scholar 

  3. F. Baader and W. Snyder. Unification Theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 8, pages 445–532. 2001.

    Google Scholar 

  4. L. Bachmair and H. Ganzinger. Resolution Theorem Proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2, pages 19–99. 2001.

    Google Scholar 

  5. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic Paramodulation. Information and Computation, 121(2):172–192, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  6. C. Beeri and R. Ramakrishnan. On the power of magic. In Proc. PODS ’87, pages 269–283, San Diego, CA, USA, 1987.

    Google Scholar 

  7. A. Borgida. On the Relative Expressiveness of Description Logics and Predicate Logics. Artificial Intelligence, 82(1–2):353–367, 1996.

    Article  MathSciNet  Google Scholar 

  8. M. Buchheit, F. M. Donini, and A. Schaerf. Decidable Reasoning in Terminological Knowledge Representation Systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.

    MathSciNet  MATH  Google Scholar 

  9. M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM, 5(7):394–397, 1962.

    Article  MathSciNet  MATH  Google Scholar 

  10. N. Dershowitz and D. A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 9, pages 535–610. 2001.

    Google Scholar 

  11. T. Eiter, G. Gottlob, and H. Mannila. Disjunctive Datalog. ACM Transactions on Database Systems, 22(3):364–418, 1997.

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  13. U. Hustadt, B. Motik, and U. Sattler. Reducing \({\mathcal{S}\mathcal{H}\mathcal{I}\mathcal{Q}}^{-}\) Description Logic to Disjunctive Datalog Programs. In Proc. KR 2004, pages 152–162, Whistler, Canada, 2004.

    Google Scholar 

  14. U. Hustadt, B. Motik, and U. Sattler. A Decomposition Rule for Decision Procedures by Resolution-based Calculi. In Proc. LPAR 2004, pages 21–35, Uruguay, 2005.

    Google Scholar 

  15. U. Hustadt, B. Motik, and U. Sattler. Data Complexity of Reasoning in Very Expressive Description Logics. In Proc. IJCAI 2005, pages 466–471, Edinburgh, UK, 2005.

    Google Scholar 

  16. U. Hustadt and R. A. Schmidt. On the Relation of Resolution and Tableaux Proof Systems for Description Logics. In Proc. IJCAI ’99, pages 202–207, Stockhom, Sweden, 1999.

    Google Scholar 

  17. W. H. Joyner. Resolution Strategies as Decision Procedures. Journal of the ACM, 23(3):398–417, 1976.

    Article  MathSciNet  MATH  Google Scholar 

  18. Y. Kazakov and H. de Nivelle. A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. In Proc. IJCAR 2004, pages 122–136, Cork, Ireland, 2004.

    Google Scholar 

  19. Y. Kazakov and B. Motik. A Resolution-Based Decision Procedure for \(\mathcal{S}\mathcal{H}\mathcal{O}\mathcal{I}\mathcal{Q}\). In Proc. IJCAR 2006, pages 662–667, Seattle, WA, USA, 2006.

    Google Scholar 

  20. O. Kutz, I. Horrocks, and U. Sattler. The Even More Irresistible SROIQ. In Proc. KR 2006, pages 68–78, Lake District, UK, 2006.

    Google Scholar 

  21. C. Lutz and U. Sattler. The Complexity of Reasoning with Boolean Modal Logics. In Proc. AiML 2000, pages 329–348, Leipzig, Germany, 2001.

    Google Scholar 

  22. B. Motik. Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Univesität Karlsruhe (TH), Karlsruhe, Germany, January 2006.

    Google Scholar 

  23. B. Motik and U. Sattler. A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes. In Proc. LPAR 2006, pages 227–241, Cambodia, 2006.

    Google Scholar 

  24. R. Nieuwenhuis and A. Rubio. Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation, 19(4):312–351, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  25. H. De Nivelle, R. A. Schmidt, and U. Hustadt. Resolution-Based Methods for Modal Logics. Logic Journal of the IGPL, 8(3):265–292, 2000.

    Article  MathSciNet  MATH  Google Scholar 

  26. A. Nonnengart and C. Weidenbach. Computing Small Clause Normal Forms. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 6, pages 335–367. 2001.

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  28. A. Riazanov and A. Voronkov. The design and implementation of VAMPIRE. AI Communications, 15(2–3):91–110, 2002.

    MATH  Google Scholar 

  29. R. A. Schmidt and U. Hustadt. A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In Proc. CADE-19, pages 412–426, USA, 2003.

    Google Scholar 

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

    Google Scholar 

  31. M. Vardi. The Complexity of Relational Query Languages. In Proc. STOC ’82, pages 137–146, San Francisco, CA, USA, 1982.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, UK

    Boris Motik

Authors
  1. Boris Motik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Boris Motik .

Editor information

Editors and Affiliations

  1. Inst. Informatik, Universität Koblenz-Landau, Universitaetsstr. 1, Koblenz, 56016, Germany

    Steffen Staab

  2. Inst. Angewandte Informatik und, Universität Karlsruhe, Karlsruhe, 76128, Germany

    Rudi Studer

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Motik, B. (2009). Resolution-Based Reasoning for Ontologies. In: Staab, S., Studer, R. (eds) Handbook on Ontologies. International Handbooks on Information Systems. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92673-3_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92673-3_24

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70999-2

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation