Probabilistic Description Logic as a Fragment of Probabilistic First-Order Logic
Final Report Abstract
Beschreibungslogiken dienen der Formulierung von Weltwissen in maschinenverarbeitbarer Form; sie verwenden dabei Dialekte eines verbreiteten logischen Formalismus, der sogenannten Modallogik. Während Standardbeschreibungslogiken formal gesehen ausschließlich mit unverrückbarem und sicherem Wissen befasst sind, besteht seit Längerem Interesse an Varianten, die etwa Vagheit, Ausnahmebehaftetheit oder Unsicherheit einfangen. Gegenstand des Projekts ProbDL ist im Wesentlichen der letztere Aspekt, d.h. die Entwicklung von Logiken für unsicheres Wissen im Sinne der Wahrscheinlichkeitstheorie sowie das Vorantreiben der Metatheorie solcher Logiken, unter anderem hinsichtlich der Analyse ihrer Ausdrucksstärke und der Komplexität und Algorithmik ihrer Schlussfolgerungsprobleme. Wahrscheinlichkeitsbasierte Logiken können als Wahrheitswerte (unter anderem) die klassischen binären Wahrheitswerte wahr/falsch verwenden oder reellwertige Wahrscheinlichkeitswerte zwischen 0 und 1, die dann als Wahrscheinlichkeiten, als erwartete Wahrscheinlichkeiten, oder allgemeiner als graduelle Wahrheitswerte verstanden werden. Logiken der ersteren Klasse beinhalten typischerweise Vergleichsoperationen auf Wahrscheinlichkeiten (“mit Wahrscheinlichkeit mindestens 90%”), während Logiken der zweiteren Form z.B. eine Modalität “wahrscheinlich” unterstützen, die als Wahrheitswert den Grad liefert, zu dem ihre Argumentformel mit “hoher” Wahrscheinlichkeit erfüllt ist. In ProbDL sind insbesondere Schlussfolgerungsalgorithmen für zweiwertige probabilistische Logiken entwickelt worden, mit besonderem Augenmerk auf hieraus folgenden oberen Komplexitätsschranken für die entsprechenden Schlussfolgerungsprobleme. Der Fokus bei der Analyse quantitativer probabilistischer Logiken lag in erster Linie auf der Ausdrucksstärke solcher Logiken. Semantische Grundlage dieser Analyse sind Begriffe von Verhaltensabstand, die gegenüber klassischen Begriffen von Verhaltensgleichheit eine quantative Verfeinerung darstellen, indem sie eben Systeme mit leicht abweichendem Verhalten nicht mehr einfach als inäquivalent klassifizieren, sondern es vielmehr ermöglichen, einen (gegebenenfalls geringen) Verhaltensabstand zwischen solchen Systemen zu messen. Im Projekt erzielte positive Resultate zur Ausdrucksstärke quantitativer probabilistischer Modallogiken besagen insbesondere, dass zum einen die Modallogik stark genug ist, um Verhaltensabstände durch Abweichungen zwischen den Wahrheitswerten von Formeln zu messen, und zum anderen, dass das modale Fragment einer entsprechenden erststufigen probabilistischen Prädikatenlogik im Wesentlichen (in einem formal präzisen Sinn) gerade das Fragment ist, das die Verhaltensdistanz respektiert.
Publications
- A characterization theorem for a modal description logic. In Carles Sierra, ed., Proc. 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, pp. 1304–1310. ijcai.org, 2017
Paul Wild and Lutz Schröder
(See online at https://doi.org/10.24963/ijcai.2017/181) - Probabilistic description logics for subjective uncertainty. J. Artif. Intell. Res. (JAIR), 58:1–66, 2017
Víctor Gutiérrez-Basulto, Jean Christoph Jung, Carsten Lutz, and Lutz Schröder
(See online at https://doi.org/10.1613/jair.5222) - Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, eds., Proc. 31st International Conference on Concurrency Theory, CONCUR 2020, vol. 171 of LIPIcs, pp. 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020
Paul Wild and Lutz Schröder
- Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Daniela Petrisan and Jurriaan Rot, eds., Proc. 15th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS 2020, vol. 12094 of LNCS, pp. 133–154. Springer, 2020
Barbara König, Christina Mika-Michalski, and Lutz Schröder
(See online at https://doi.org/10.1007/978-3-030-57201-3_8) - A quantified coalgebraic van benthem theorem. In Stefan Kiefer and Christine Tasson, eds., Proc. 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021, vol. 12650 of LNCS, pp. 551–571. Springer, 2021
Paul Wild and Lutz Schröder
(See online at https://doi.org/10.1007/978-3-030-71995-1_28) - Coalgebraic reasoning with global assumptions in arithmetic modal logics. ACM Trans. Comput. Log.
Clemens Kupke, Dirk Pattinson, and Lutz Schröder
(See online at https://doi.org/10.48550/arXiv.2009.00971)
