Unifikation in Beschreibungslogiken zur Vermeidung von Redundanzen in medizinischen Ontologien

• Antragsteller: Professor Dr.-Ing. Franz Baader
• Fachliche Zuordnung: Theoretische Informatik ; Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
• Förderung: Förderung von 2009 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 151328653

• Erstellungsjahr: 2018

Zusammenfassung der Projektergebnisse

Unifikation in Beschreibungslogiken ist ein nicht-standard Schlussfolgerungsproblem, das dazu verwendet werden kann, den Aufbau und die Wartung von Ontologien zu unterstützen. Vor Beginn des Projektes war es uns gelungen nachzuweisen, dass Unifikation in der Beschreibungslogik EL, die z.B. zur Definition von medizinischen Ontologien wie SNOMED CT verwendet wird, ein NP-vollständiges Problem ist. In der ersten Projektphase gelang es uns zum einen, praktikable Algorithmen für dieses Problem zu entwickeln und zu implementieren. Zum anderen versuchten wir, diese Unifikationsalgorithmen auf Unifikation in EL bzgl. allgemeiner Ontologien zu erweitern. Dies gelang uns aber nur für eingeschränkte Formen von Ontologien, bei denen gewisse Arten von Zyklen verboten sind. In der zweiten Projektphase versuchten wir, positive Resultate für uneingeschränkte EL-Ontologien zu erhalten, was uns aber nur für gewisse Varianten der Unifikation (Matching, hybride Unifikation) gelungen ist. Beim Matching betrachten wir Äquivalenz- und Subsumtionsconstraints, bei denen eine Seite keine Variablen enthält. Wir konnten zeigen, dass Matching in EL auch bzgl. uneingeschränkter Ontologien NP-vollständig ist. Zusätzlich konnten wir zwei eingeschränkte Arten von Matchingproblemen bestimmen, für die Lösbarkeit polynomiell entscheidbar ist. Bei der hybriden Unifikation erlaubt man als Lösungen nicht nur Substitutionen (d.h. azyklische TBoxen), sondern auch zyklische Unifikatoren (d.h. zyklische TBoxen), wobei als Semantik für diese zyklischen Lösungen die in der Literatur eingeführte hybride Semantik verwendet wird. Wir konnten zeigen, dass hybride Unifikation in EL auch bzgl. uneingeschränkter Ontologien NP-vollständig ist und einen praktikablen Algorithmus zur Lösung dieses Problems angeben. Ein weiterer Schwerpunkt unserer Arbeiten in der zweiten Projektphase war die Untersuchung von Disunifikation in EL. Bei der Disunifikation hat man zusätzlich zu den positiven Unifikationsconstraints auch negative Constraints, mit denen man z.B. unerwünschte, in der Anwendungsdomäne nicht sinnvolle Unifikatoren verhindern kann. Leider ist es uns nicht gelungen, Entscheidbarkeit der Disunifikation in EL im allgemeinen Fall zu zeigen, da die negativen Constraints die für die Unifikation wichtige Lokalitätseigenschaft zerstören. Wir betrachteten daher den eingschränkten Fall des Dismatching, bei dem man ein allgemeines Unifikationsproblem um Dissubsumtionen erweitert, bei denen eine Seite keine Variablen enthält. Wir konnten zeigen, dass Lösbarkeit eines solchen Dismatchingproblems auf lokale Disunifikation reduzierbar ist und für letzteres Problem praktikable NP-Algorithmen angeben. Auf praktischer Seite untersuchten wir in der zweiten Projektphase die Verwendung von Disunifikation in EL zur Erzeugung von Konzepten in medizinischen Ontologien. Die Idee ist dabei, dass man statt einer Definition des Konzeptes nur dessen gewünschte Lage in der bereits vorhandenen Konzepthierarchie angibt. Diese Lage wird dazu verwendet, ein Disunifikationsproblem zu generieren, dessen (lokale) Lösungen dann als Kandidaten für die Definition des Konzeptes vorgeschlagen werden. In unseren Experimenten entfernten wir bereits existierende Konzepte aus SNOMED CT und versuchten, diese durch unseren Ansatz zu reproduzieren. Obwohl die exakt selbe Definition nur in 6% der Testfälle reproduziert wurde, vermuten wir, dass häufig „ähnliche“ Definitionen erzeugt wurden. Dies muss aber noch unter Verwendung geeigneter Ähnlichkeitmaße für EL-Konzepte genauer untersucht werden.

Projektbezogene Publikationen (Auswahl)

• Hybrid unification in the Description Logic EL. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Proc. of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), volume 8152 of Lecture Notes in Computer Science, pages 295–310. Springer-Verlag, 2013
  Franz Baader, Oliver Fernández Gil, and Barbara Morawska
  (Siehe online unter https://doi.org/10.1007/978-3-642-40885-4_21)
• Matching with respect to general concept inclusions in the Description Logic EL. In Carsten Lutz and Michael Thielscher, editors, Proc. of the 37th German Conference on Artificial Intelligence (KI’14), volume 8736 of Lecture Notes in Artificial Intelligence, pages 135–146. Springer-Verlag, 2014
  Franz Baader and Barbara Morawska
  (Siehe online unter https://doi.org/10.1007/978-3-319-11206-0_14)
• Extending unification in EL to disunification: The case of dismatching and local disunification. Logical Methods in Computer Science, 12(4:1):1–28, 2016
  Franz Baader, Stefan Borgwardt, and Barbara Morawska
  (Siehe online unter https://doi.org/10.2168/LMCS-12(4:1)2016)
• Constructing SNOMED CT Concepts via Disunification. LTCS-Report 17-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017
  Franz Baader, Stefan Borgwardt, and Barbara Morawska