Konservative Erweiterungen in Onologiesprachen: Jenseits von Beschreibungslogik

• Antragsteller: Professor Dr. Carsten Lutz; Professor Dr. Thomas Schneider
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 264279960

• Erstellungsjahr: 2019

Zusammenfassung der Projektergebnisse

Ontologien sind logische Theorien, die Wissen über eine Anwendungsdomäne zur Verfügung stellen. Verwendet werden sie unter anderem in der Wissensrepräsentation, in intelligenten Datenbanken sowie in vielen wissenschaftlichen Disziplinen wie z. B. der Bio- und Medizininformatik, den Lebenswissenschaften und der Linguistik. Es gibt eine beachtliche Vielzahl von Ontologiesprachen, wobei Beschreibungslogiken (BLen) eine Schlüsselrolle spielen, entscheidbare Fragmente der Prädikatenlogik erster Stufe (first-order logic, FO), die der standardisierten Web-Ontologiesprache OWL zugrunde liegen. Ausdrucksstärkere Fragmente von FO wie das guarded fragment (GF) und das Zwei-Variablen-Fragment FO2 bilden eine wichtige Generalisierung von BLen und werden bisweilen auch direkt als Ontologiesprachen genutzt. Das Entwickeln einer Ontologie ist eine komplexe Aufgabe, die der Unterstützung durch geeignete Schlussfolgerungsdienste bedarf. Insbesondere konservative Erweiterungen (conservative extensions) bilden eine wichtige Grundlage für verschiedene Aspekte des Ontologieentwurfs wie z.B. Verfeinerung, Versionskontrolle und Modularität. In den vergangenen Jahren wurde gezeigt, dass konservative Erweiterungen in vielen BLen entscheidbar sind, und zwar sowohl die deduktive Variante (dKEs) als auch die anfragebasierte (query conservative extensions, qKEs). Das Projekt CEO verfolgte zwei Hauptziele: zum einen sollten wichtige offene Probleme betreffs konservativer Erweiterungen in BLen gelöst werden; zum anderen wollten wir ein Verständnis dafür gewinnen, inwieweit sich die Entscheidbarkeit von dKEs und qKEs über BLen hinaus auf FO-Fragmente wie GF und FO2 überträgt. Das Projekt CEO hat grundlegende Resultate bezüglich der Grenzen des Entscheidens konservativer Erweiterungen geliefert, einschließlich der folgenden Highlights. Wir haben gezeigt, dass dKEs in GF und FO2 und sogar im Drei-Variablen-Fragment von GF unentscheidbar sind. Wir haben außerdem gezeigt, dass qKEs für ausdrucksstarke BLen wie ALC unter der Verwendung konjunktiver Anfragen (conjunctive queries, CQs) als Anfragesprache ebenfalls unentscheidbar sind, woraus auch Unentscheidbarkeit von qKEs in GF und FO2 folgt. Somit ist Entscheidbarkeit konservativer Erweiterungen viel weniger robust als Entscheidbarkeit von Erfüllbarkeit. Diese negativen Resultate werden ergänzt durch positive Resultate, mit denen wir klären, dass dKEs im Zwei-Variablen-Fragment von GF (d. h. im Schnitt von GF und FO2) entscheidbar sind und dass qKEs zwischen Wissensbasen in ALC entscheidbar sind, wenn Vereinigungen von CQs als Anfragesprache verwendet werden. Diese Resultate legen nahe, dass für die Entscheidbarkeit von dKEs eine starke Baummodelleigenschaft benötigt wird und dass für die Entscheidbarkeit von qKEs in ausdrucksstarken Ontologiesprachen die Anfragesprache mit Disjunktion ausgestattet sein sollte.

Projektbezogene Publikationen (Auswahl)

• (2020) Conservative extensions in horn description logics with inverse roles. Journal of Artificial Intelligence Research 68 365-411
  Jung, Jean Christoph; Lutz, Carsten; Martel, Mauricio; Schneider, Thomas
  
• Query-based entailment and inseparability for ALC ontologies. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI’16), pages 1001–1007. IJCAI/AAAI Press, 2016
  Elena Botoeva, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev
  
• Relation-changing logics as fragments of hybrid logics. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF’16), volume 226 of EPTCS, pages 16–29, 2016
  Carlos Areces, Raul Fervari, Guillaume Hoffmann, and Mauricio Martel
  
• Conservative extensions in guarded and two-variable fragments. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming (ICALP’17), volume 80 of LIPIcs, pages 108:1–108:14. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2017
  Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, and Frank Wolter
  
• Query conservative extensions in Horn description logics with inverse roles. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI’17), pages 1116–1122. ijcai.org, 2017
  Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider
  
• Querying the unary negation fragment with regular path expressions. In Benny Kimelfeld and Yael Amsterdamer, editors, Proceedings of the 21st International Conference on Database Theory (ICDT’18), volume 98 of LIPIcs, pages 15:1–15:18. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2018
  Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider
  
• Satisfiability for relation-changing logics. Journal of Logic and Computation, 28(7):1443–1470, 2018
  Carlos Areces, Raul Fervari, Guillaume Hoffmann, and Mauricio Martel
  
• Query inseparability for ALC ontologies. Artificial Intelligence, 272:1–51, 2019
  Elena Botoeva, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev