Complexity and Expressivity of Dependence Logic Extensions

Vorschau

Leseprobe, PDF (81 KB)
Inhaltsverzeichnis, PDF (56 KB)

Dependence Logic (D) wurde 2007 von Jouko Väänänen erstmals vorgestellt. Hierbei handelte es sich um eine Logik, welche die Prädikatenlogik der ersten Stufe um das sogenannte dependence Atom (in Zeichen =(t_1,…,t_n)) erweitert. Es ist erfüllt, wenn die funktionale Abhängigkeit des Terms t_n von den Termen t_1,…, t_n-1 gegeben ist, d.h. wenn t_n eine Funktion von t_1,…, t_n-1 ist. 2009 wurde eine modale Version der dependence Logik (MDL) von Abramsky und Väänänen erstmals vorgestellt.
In dieser Arbeit betrachten wir sowohl modale als sich die prädikatenlogische Variante.

In Kapitel 3 stellen wir die Erweiterungen der dependence Logik um die Quantoren M und ein Paritätsquantor.

Der Quantor M ist erfüllt, wenn mindestens die Hälfte aller Belegungen für die quantifizierte Variable wahr ist. Der Paritätsquantor wird wahr, wenn eine gerade Anzahl von Belegungen der quantifizierten Variablen wahr ist. In Kapitel 3 zeigen wir, dass dependence Logik erweitert um M mit der Hierarchie der Zählklassen PP (CH) übereinstimmt und dependence Logik erweitert um den Paritätsquantor mit der Komplexitätsklasse parityP.

Kapitel 4 beschäftigt sich mit erweiterter modalen dependence Logik (EMDL), welche auf der von Sevenster und Väänänen vorgestellten modalen dependence Logik beruht. Hierbei wird das dependence Atom =(p_1,…, p_n), welches in MDL nur auf atomare Propositionen p_1,…,p_n angewendet wird, durch ein neues dependence Atom ersetzt, welches auch modalligische Formeln beinhalten kann. Wir zeigen, dass die Komplexität des Modellprüfungsproblems sowie die Komplexität des Erfüllbarkeitsproblems nicht schwieriger sind, als die korrespondierenden Probleme auf der Logik MDL. Außerdem zeigen wir, dass es EMDL Formeln gibt, die nicht durch MDL Formeln abgebildet werden können.

In Kapitel 5 wird wieder eine Variante der prädikatenlogischen dependence Logik vorgestellt. Diese Boole’scher dependence Logik BD wird mit sogenannten partially ordered connectives verglichen, welche von Henkin vorgestellt wurden. Dabei wird gezeigt, dass die Logiken sowie ihre Fragmente äquivalent sind. Des Weiteren wird gezeigt, dass Boole’sche dependence Logik eine strikte Trennung zu ihren Logikfragmenten aufweist. Das heißt, dass es Formeln in einem Fragment der Logik gibt, die sich nicht in einem kleineren Fragment der Logik darstellen lassen.