Darstellung und Schlussfolgerung in Beschreibungslogiken mit Zahlen

Projekttitel: Kombination von logischem und numerischem Denken – Darstellung und Schlussfolgerungen in Beschreibungslogiken mit Zahlen

Projektdauer: 2022 – 2025

Forschungsbereich: Mathematische Grundlagen und statistisches Lernen

Beschreibungslogiken (Description Logics, DLs) sind eine bedeutende Familie symbolischer KI-Formalismen, die die Grundlage der Web Ontology Language (OWL) bilden und in vielen Anwendungsbereichen zur Spezifizierung und zum Schlussfolgern über Ontologien verwendet werden. Klassische DLs können jedoch bestimmte anwendungsrelevante numerische Einschränkungen nicht direkt ausdrücken. Um dieses Defizit zu beheben, wurden in der Literatur verschiedene Arten numerischer Erweiterungen von DLs vorgeschlagen, wie zum Beispiel:

1. Beschreibungslogiken mit Kardinalitätsbeschränkungen (die z. B. ausdrücken können, dass ein bestimmtes Schaltgatter mehr Eingänge als Ausgänge hat)
2. Beschreibungslogiken mit konkreten Domänenbeschränkungen (die z. B. die Herzfrequenz eines Patienten darstellen und mit einem Schwellenwert oder anderen Messwerten vergleichen können)
3. Probabilistische Erweiterungen von Beschreibungslogiken (die z. B. die Wahrscheinlichkeit ausdrücken können, dass ein Protein, das an einen bestimmten Molekültyp bindet, eine bestimmte Eigenschaft von Interesse aufweist)

Ziel dieses Projekts ist es, die formalen Eigenschaften solcher quantitativen Erweiterungen von DLs zu untersuchen und neue mathematische Werkzeuge zu entwickeln, die solche Untersuchungen unterstützen.

Ziele

Dieses Projekt hat drei Hauptziele:

1. Entwicklung mathematischer Werkzeuge zur Analyse der Ausdruckskraft quantitativer Beschreibungslogiken und deren Anwendung auf die drei oben genannten Arten numerischer Erweiterungen von Beschreibungslogiken.
2. Untersuchung des Problems der Modellzählung für Ontologien, die in solchen Logiken geschrieben sind, und deren Anwendung.
3. Kombination von Schlussfolgerungssystemen und algorithmischen Techniken für Beschreibungslogiken mit Solvern aus dem Bereich der Satisfiability Modulo Theories (SMT), um praxisnäher ausgerichtete Schlussfolgerungssysteme für quantitative Beschreibungslogiken zu erhalten.

Problemstellung

• Können wir bekannte Ergebnisse aus der (endlichen) Modelltheorie nutzen, um die Ausdruckskraft von Beschreibungslogiken mit Kardinalitätsbeschränkungen und konkreten Domänenbeschränkungen zu charakterisieren und die Modellzählung in diesen Sprachen zu verstehen? Falls nicht, welche neuen Konzepte und Theorien müssen entwickelt werden?
• Können wir Algorithmen oder Kombinationen von Schlussfolgerungssystemen entwerfen, die für die Implementierung und den Einsatz von logischen Schlussfolgerungssystemen auf Ontologien geeignet sind, die ausdrucksstarke Kardinalitätsbeschränkungen oder konkrete Domänenbeschränkungen enthalten?

Technologie

Die Forschung zu den Zielen (1) und (2) ist theoretischer Natur und stützt sich auf Methoden aus der mathematischen Logik, der Modallogik und der (endlichen) Modelltheorie. Um Ziel (3) anzugehen, werden wir Methoden aus den Bereichen Wissensrepräsentation und Schlussfolgerung (z. B. tableau- und konsequenzbasierte Schlussfolgerungssysteme) mit Methoden aus den Bereichen automatisierte Deduktion und formale Methoden (z. B. SMT-Löser) kombinieren, um Schlussfolgerungssysteme für quantitative DLs zu entwickeln.

Ausblick

Dieses Projekt wird sowohl das Verständnis der formalen Eigenschaften quantitativer DLs als auch deren Einsatzmöglichkeiten in Anwendungen, die solche DLs erfordern, verbessern.

Publikationen

• Franz Baader and Filippo De Bortoli: The Abstract Expressive Power of First-Order and Description Logics with Concrete Domains. In The 39th ACM/SIGAPP Symposium on Applied Computing (SAC ’24), April 8–12, 2024, Avila, Spain. ACM, New York, NY, USA, Article 4, 8 pages. https://doi.org/10.1145/3605098.3635984 (To appear)
• Franz Baader and Filippo De Bortoli: On the Abstract Expressive Power of Description Logics with Concrete Domains. In Oliver Kutz and Ana Ozaki (eds.). Proceedings of the 36th International Workshop on Description Logics (DL’23), volume 3515 of CEUR Workshop Proceedings. Rhodes, Greece, CEUR-WS, 2023. https://ceur-ws.org/Vol-3515/paper-3.pdf
• Franz Baader, Jakub Rydval: Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains. J. Autom. Reason. 66(3): 357-407 (2022). https://doi.org/10.1007/s10817-022-09626-2

Team

Teamleitung

• Prof. Dr.-Ing. Franz Baader

Teammitglieder

• Dr. Anton Claußnitzer
• Filippo De Bortoli

Partner

• Technische Universität Dresden (TUD)