nach oben

Erschienen in:

2009 | OriginalPaper | Buchkapitel

Resolution-Based Reasoning for Ontologies

verfasst von : Boris Motik

Erschienen in: Handbook on Ontologies

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Tableau-Based Reasoning

Nächstes Kapitel Ontology Repositories

http://kaon2.semanticweb.org/

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

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.

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.

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.

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

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

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

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

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

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.

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

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.

Titel: Resolution-Based Reasoning for Ontologies
verfasst von: Boris Motik
Verlag: Springer Berlin Heidelberg
Buch: Handbook on Ontologies
Print ISBN: 978-3-540-70999-2

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

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

Springer Professional

Summary

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"