Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
What Is an Ontology? Read chapter Read first chapter

2009 | OriginalPaper | Chapter

Resolution-Based Reasoning for Ontologies

Author : Boris Motik

Published in: Handbook on Ontologies

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Tableau-Based Reasoning
next chapter Ontology Repositories
Footnotes
Literature
1.
S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison Wesley, 1995.
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.
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.
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.
5.
6.
C. Beeri and R. Ramakrishnan. On the power of magic. In Proc. PODS ’87, pages 269–283, San Diego, CA, USA, 1987.
7.
A. Borgida. On the Relative Expressiveness of Description Logics and Predicate Logics. Artificial Intelligence, 82(1–2):353–367, 1996.MathSciNetCrossRef
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.MathSciNetMATH
9.
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.
11.
T. Eiter, G. Gottlob, and H. Mannila. Disjunctive Datalog. ACM Transactions on Database Systems, 22(3):364–418, 1997.CrossRef
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.MathSciNetCrossRefMATH
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.
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.
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.
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.
17.
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.
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.
20.
O. Kutz, I. Horrocks, and U. Sattler. The Even More Irresistible SROIQ. In Proc. KR 2006, pages 68–78, Lake District, UK, 2006.
21.
C. Lutz and U. Sattler. The Complexity of Reasoning with Boolean Modal Logics. In Proc. AiML 2000, pages 329–348, Leipzig, Germany, 2001.
22.
B. Motik. Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Univesität Karlsruhe (TH), Karlsruhe, Germany, January 2006.
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.
24.
R. Nieuwenhuis and A. Rubio. Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation, 19(4):312–351, 1995.MathSciNetCrossRefMATH
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.MathSciNetCrossRefMATH
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.
27.
D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Logic and Computation, 2(3):293–304, 1986.MathSciNetCrossRefMATH
28.
A. Riazanov and A. Voronkov. The design and implementation of VAMPIRE. AI Communications, 15(2–3):91–110, 2002.MATH
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.
30.
S. Tobies. Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, Germany, 2001.
31.
M. Vardi. The Complexity of Relational Query Languages. In Proc. STOC ’82, pages 137–146, San Francisco, CA, USA, 1982.
Metadata
Title
Resolution-Based Reasoning for Ontologies
Author
Boris Motik
Copyright Year
2009
Publisher
Springer Berlin Heidelberg
Book
Handbook on Ontologies

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

Electronic ISBN: 978-3-540-92673-3

Copyright Year: 2009

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

Premium Partner

    Image Credits