Logics with Multiteam Semantics

Kontakt

Telefon

work
+49 241 80 21722

E-Mail

E-Mail
  at work Urheberrecht: Stefan Hense

Klassische Logiken wie die Logik erster Stufe modellieren Aussagen über Strukturen wie Graphen oder Datenbanken. Diese können jedoch nicht über die Abhängigkeiten verschiedener Variablen sprechen. Die ersten Ansätze, Logiken mit dieser Ausdrucksstärke zu versehen, kamen von Henkin, Enderton und Walkoe. Die Semantik der entstandenen Logiken kann mittels der Model-Checking-Spiele erklärt werden, ein Spiel zwischen zwei Spielern, die versuchen nachzuweisen dass die gegebene Formel die betrachtete Struktur erfüllt, oder nicht. Um die Abhängigkeiten (bzw. Unabhängigkeiten) zu modellieren war es den Spielern gegebenenfalls nicht möglich ihre Züge auf die des Gegners anzupassen. Väänänen gab mit der dependence logic einen neuen Ansatz, bei dem Abhängigkeiten als atomare Aussagen aufgefasst wurden. Dafür müssen alle Informationen über die Variablenbelegungen verfügbar sein, weshalb statt einer Zuweisung eine Menge dieser betrachtet wird. Eine Schwäche ist, dass kein Wissen über die Anzahl der Vorkommnisse der Zuweisungen vorhanden ist, sondern lediglich deren Existenz. Oftmals ist aber genau dies relevant, etwa bei einer Wahl die Anzahlen der Stimmen für einen Kandidaten. Um dies zu modellieren haben wir uns dafür entschieden statt einer Menge eine Multimenge an Zuweisungen zu betrachten, woraus Logiken mit Multiteam-Semantik resultieren, welche aussagen über statistische Abhängigkeiten in Daten machen können, oder mit denen Unsicherheit in Datensätzen modelliert werden können. Ziel der Arbeit ist es eine fundierte Grundlage dieser Logiken zu schaffen.