Navigation Forschung Lehre Personen Publikationen Kontakt   Reasoning Services: Tableau-Beweiser für Beschreibungslogiken Veranstalter Zeit/Ort Inhalt Literatur Links Wir freuen uns über Kommentare und Hinweise zu diesen Seiten.

18.335 Projekt: Reasoning Services: Tableau-Beweiser für Beschreibungslogiken Wintersemester 2006/07 Veranstalter Carola Eschenbach, Özgür Özçep Zeit/Ort Mi. 12-15 D-129, Fr. 12-15 F-635 Aktuelles Der entwickelte Beweiser ist jetzt online. KVV-Eintrag Inhalt In diesem Projekt werden wir einen einfachen (in Java implementierten) aussagenlogischen Theorembeweiser durch verschiedene Ergänzungen und Optimierungen zu einem beschreibungslogischen Theorembeweiser erweitern. Die Erweiterungen betreffen z.B. die verwendete Sprache und Eingabemöglichkeiten für Beispiele, das Beweis-Verfahren selbst, das mit der größeren Ausdrucksmächtigkeit umgehen muss, und die bereitgestellten 'Reasoning Services'. 'Reasoning Services' sind Dienste, die basierend auf logischen Beschreibungen Schlüsse ausführen. Beispiele solcher Dienste sind die Prüfung, ob eine Konzeptbeschreibung konsistent ist, und die Einordnung eines neuen Konzeptes in eine bestehende Taxonomie von Konzepten. Für die Implementation von Beweisverfahren für Beschreibungslogiken haben sich Tableau-Beweiser, die auch in der Vorlesung LOS ausführlich behandelt werden, bewährt. Jedoch sind eine Reihe von Optimierungsschritten erforderlich, um die Anforderungen nach Speicherplatz und Rechenzeit in einen akzeptablen Bereich zu bringen. Bei den Optimierungen werden verschiedene aus der Literatur bekannte Verfahren so umgesetzt, dass die 'logischen' Eigenschaften (Korrektheit und Vollständigkeit) nicht beeinträchtigt werden. Beschreibungslogiken erlauben die Spezifikation von komplexen Terminologien. Beispiele für Beschreibungslogiken mit unterschiedlicher Ausdrucksmächtigkeit sind zwei Sprachen der OWL-Familie, die im Rahmen des 'Semantic Web' zunehmend Verwendung finden. Literatur Baader, Franz, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi & Peter Patel-Schneider (eds.) (2003). The Description Logic Handbook. Theory, Implementation and Application. Cambridge UP: Cambridge, NY. Nardi, Daniele & Ronald J. Brachman (2003). An introduction to description logics. In F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi & P. Patel-Schneider (2003, eds.) (pp. 1--40) Baader, Franz & Werner Nutt (2003). Basic description logics. In F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi & P. Patel-Schneider (2003, eds.) (pp. 43--95). Baader, Franz (2003). Appendix 1. Description logic terminology. In F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi & P. Patel-Schneider (eds., 2003) (pp. 485--495). Fitting, Melvin (1999). Introduction. In M.D'Agostino, D.M. Gabbay, R.Hähnle und J. Posegga (eds.): Handbook of Tableau Methods (pp 1-43). Kluwer Academic Publishers: Dordrecht. (.pdf) Baader, Franz & Ulrike Sattler (2001). An overview of tableau algorithms for description logics. Studia Logica 69. 5--40. (citeseer) Horrocks, Ian (1998). The FaCT system. In H. de Swart (ed.) Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'98 (pp. 307--312). Springer-Verlag. (citeseer) Horrocks, Ian R. (1998). Using an expressive description logic: FaCT or fiction?. In Anthony G. Cohn, Lenhart Schubert & Stuart C. Shapiro (eds.) KR'98: Principles of Knowledge Representation and Reasoning (pp. 636--645). Morgan Kaufmann: San Francisco, California. (citeseer) Horrocks, Ian & Peter Patel-Schneider (1999). Optimizing description logic subsumption. Journal of Logic and Computation 9. 267-293.(citeseer) Weitere Literatur wird bekannt gegeben. Links Das Resultat: Der Tableau-Beweiser für eine einfache Beschreibungslogik, der in dem Projekt entwickelt wurde. Der Ausgangspunkt: Der aussagenlogische Tableau-Beweiser zum Ausprobieren. Projektbericht von Arved Solth (.pdf) Projektbericht von Roland Illig (.pdf) Materialien Testmaterial Tableaux'98 Protokolle Tafelbild vom 27.10.06 (ÖÖ): Universitätsontologie (.pdf) Protokoll von A. Solth & J. Wächter vom 27.10.06: Universitätsontologie, Aufgabe a) (.pdf) und zugehörige Grafik (.pdf) Protokoll von F. Lindner & N. Beuck vom 27.10.06: Universitätsontologie, Aufgabe b) (.pdf) Protokoll von O. Gries & R. Illig vom 27.10.06: Universitätsontologie, Aufgabe c) (.pdf) Protokoll von J. Wächter & A. Solth vom 8.11.06: Diskussion Baader & Nutt (.pdf) Protokoll von O. Gries vom 10.11.06: Diskussion Baader & Nutt (.pdf) Protokoll von F. Lindner vom 15.11.06: Fortsetzung der Diskussion zu Baader & Nutt und erster Plan zur Implementation (.pdf) Protokoll von F. Lindner vom 12.1.07: Arbeitsverteilung Optimierung (.pdf) Aufgaben Aufgabe zum/am 27.10.06: Universitätsontologie (.pdf) Aufgabe zum 1.11.06: Leseanleitung Fitting (.pdf) und noch ein Link auf den Aufsatz: (.pdf) Aufgabe zum 1.11.06: Testen des aussagenlogischen TB-Beweisers (.html) Folien mit Aufgaben zm 3.11.06: Struktur des aussagenlogischen Tableaubeweisers (.pdf) Aufgabe zum 8.11.06: Leseanleitung (.pdf), Link auf den Aufsatz: (.pdf) und auch nochmal der Link auf den Appendix, ein nützliches Nachschlagewerk: (.pdf) Aufgabe zum 8.11.06: Universitätsontologie in DL (.txt) Vortragsfolien Einführung (CE/ÖÖ) (.pdf) Präsentation ReasoningServices (FL/OG) (.pdf) Präsentation Prover (JW/NB/AS) (.ppt) Abschlusspräsentation am 6.2.2007 im WSV Oberseminar (.ppt)