Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
What Is an Ontology? Kapitel lesen Erstes Kapitel lesen

2009 | OriginalPaper | Buchkapitel

Tableau-Based Reasoning

verfasst von : Ralf Möller, Volker Haarslev

Erschienen in: Handbook on Ontologies

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Summary

Tableau-based methods for satisfiability checking build the backbone of major contemporary ontology reasoning sytems. The main idea of tableau-based methods for satisfiability checking is to systematically construct a representation for a model of the input formulae. If all representations that are considered by the procedure turn out to contain an obvious contradiction, a model representation cannot be found and it is concluded that the set of formulae is unsatisfiable.
In this chapter, tableau-based reasoning methods are formally introduced. We start with a nondeterministic basic version which subsequently will be extended with optimization techniques in order to demonstrate how practical systems can be built. We also demonstrate how computed tableau structures can be exploited for other inference problems in an ontology reasoning system.

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 RDF Storage and Retrieval Systems
Nächstes Kapitel Resolution-Based Reasoning for Ontologies
Fußnoten
1
For instance, if numbers are chosen for the unique identifier, the unique identifier of the negation of a (non-negated) concept with number n could be n + 1. The encoding process must assign numbers accordingly. If (pointers to) objects are used for representing concepts, a field with a pointer to the negated concept provides for a fast implementation of neg at the cost of memory requirements probably being a little bit higher.
 
2
We use a way to construct the canonical interpretation that already considers additional concept constructors such as, say, number restrictions. In case of \(\mathcal {A}\mathcal {L}\mathcal {C}\) it would be possible to map i to its witness w in the canonical interpretation.
 
Literatur
1.
Franz Baader, Martin Buchheit, and Bernhard Hollunder. Cardinality restrictions on concepts. Artificial Intelligence, 88(1–2):195–213, 1996.CrossRefMATH
2.
Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge, 2003.
3.
Franz Baader, Enrico Franconi, Bernhard Hollunder, Bernhard Nebel, and Hans-Jürgen Profitlich. An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on. Applied Artificial Intelligence. Special Issue on Knowledge Base Management, 4: 109–132, 1994.
4.
Franz Baader and Philipp Hanschke. A schema for integrating concrete domains into concept languages. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI’91), pages 452–457, 1991.
5.
Franz Baader, Ralf Küsters, and Frank Wolter. Extensions to description logics. In [2], pages 219–261. 2003.
6.
Franz Baader and Werner Nutt. Basic description logics. In [2], pages 43–95. 2003.
7.
8.
Martin Buchheit, Francesco M. Donini, and Andrea Schaerf. Decidable reasoning in terminological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.MathSciNetMATH
9.
J. W. Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1995.
10.
V. Haarslev and R. Möller. Practical reasoning in racer with a concrete domain for linear inequations. In Proceedings of the International Workshop on Description Logics (DL-2002), Toulouse, France, April 19-21, pages 91–98, 2002.
11.
V. Haarslev, R. Möller, and M. Wessel. The description logic alcnhr+ extended with concrete domains. Technical Report FBI-HH-M-290/00, University of Hamburg, Computer Science Department, 2000.
12.
Volker Haarslev and Ralf Möller. Expressive abox reasoning with number restrictions, role hierarchies, and transitively closed roles. In Proc. of the 7th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2000), pages 273–284. Morgan Kaufmann, 2000.
13.
Volker Haarslev and Ralf Möller. High performance reasoning with very large knowledge bases: A practical case study. In Proc. of the 17th Int. Joint Conf. on Artificial Intelligence (IJCAI 2001), pages 161–168, 2001.
14.
Bernhard Hollunder and Franz Baader. Qualifying number restrictions in concept languages. In Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’91), pages 335–346, 1991.
15.
Ian Horrocks. Optimisation techniques for expressive description logics. Technical Report UMCS-97-2-1, University of Manchester, Department of Computer Science, 1997.
16.
Ian Horrocks. Using an expressive description logic: FaCT or fiction? In Proc. of the 6th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’98), pages 636–647, 1998.
17.
Ian Horrocks. Implementation and optimization techniques. In [2], pages 306–346. 2003.
18.
Ian Horrocks, Oliver Kutz, and Ulrike Sattler. The even more irresistible \(\mathcal {S}\mathcal {R}\mathcal {O}\mathcal {I}\mathcal {Q}\). In Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006), pages 57–67. AAAI Press, 2006.
19.
Ian Horrocks and Peter F. Patel-Schneider. Optimizing description logic subsumption. Journal of Logic and Computation, 9(3):267–293, 1999.MathSciNetCrossRefMATH
20.
Ian Horrocks and Ulrike Sattler. A tableaux decision procedure for \(\mathcal {S}\mathcal {H}\mathcal {O}\mathcal {I}\mathcal {Q}\). In Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI 2005), pages 448–453, 2005.
21.
Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Reasoning with individuals for the description logic \(\mathcal {S}\mathcal {H}\mathcal {I}\mathcal {Q}\). In David McAllester, editor, Proc. of the 17th Int. Conf. on Automated Deduction (CADE 2000), volume 1831 of Lecture Notes in Computer Science, pages 482–496. Springer, 2000.
22.
Ian Horrocks and Stephan Tobies. Reasoning with axioms: Theory and practice. In Proc. of the 7th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2000), pages 285–296, 2000.
23.
Alexander. K. Hudek and Grant Weddell. Binary absorption in tableaux-based reasoning for description logics. In Proc. of the 2006 Description Logic Workshop (DL 2006). CEUR Electronic Workshop Proceedings, http://​ceur-ws.​org/​Vol-189/, 2006.
24.
C. Lutz. PSpace reasoning with the description logic \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}(\mathcal {D})\). Logic Journal of the IGPL, 10(5):535–568, 2002.MathSciNetCrossRef
25.
C. Lutz and M. Milicic. A tableau algorithm for description logics with concrete domains and general tboxes. Journal of Automated Reasoning, 2006. To appear.
26.
Ralf Möller and Volker Haarslev. Description logic systems. In [2], pages 282–305. 2003.
27.
Ulrike Sattler. A concept language extended with different kinds of transitive roles. In Günter Görz and Steffen Hölldobler, editors, Proc. of the 20th German Annual Conf. on Artificial Intelligence (KI’96), volume 1137 of Lecture Notes in Artificial Intelligence, pages 333–345. Springer, 1996.
28.
Andrea Schaerf. Reasoning with individuals in concept languages. In Proc. of the 3rd Conf. of the Ital. Assoc. for Artificial Intelligence (AIIA’93), Lecture Notes in Artificial Intelligence. Springer, 1993.
29.
Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1):1–26, 1991.MathSciNetCrossRefMATH
30.
Stephan Tobies. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. Journal of Artificial Intelligence Research, 12:199–217, 2000.MathSciNetMATH
31.
Dmitry Tsarkov and Ian Horrocks. Efficient reasoning with range and domain constraints. In Proc. of the 2004 Description Logic Workshop (DL 2004), pages 41–50, 2004.
32.
Dmitry Tsarkov, Ian Horrocks, and Peter F. Patel-Schneider. Optimizing terminological reasoning for expressive description logics. Journal of Automated Reasoning, 39(3):277–316, 2007.MathSciNetCrossRefMATH
Metadaten
Titel
Tableau-Based Reasoning
verfasst von
Ralf Möller
Volker Haarslev
Copyright-Jahr
2009
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_23