Algebraische Charakterisierungen von positiver Quantorenalternierung bei Zwei-Variablen-Logik

Abstract

Thérien und Wilke zeigten in einer Arbeit von 1998, dass Zwei-Variablen-Logik erster Stufe (FO2) einer entscheidbaren Klasse endlicher Monoide entspricht. Insbesondere lässt sich damit für jede reguläre Sprache entscheiden, ob sie in FO2 definierbar ist. Dieses Entscheidbarkeitsresultat konnte im vergangenen Jahr von Weil und Kufleitner auf die Alternierungshierarchie innerhalb von FO2 ausgedehnt werden. In einer aktuellen Arbeit von Lauser und Kufleitner wurde dieses Ergebnis noch weiter verfeinert. Sie konnten zeigen, dass die positive Alternierungshierarchie innerhalb von FO2 entscheidbar ist. Krebs und Straubing konnten mit einem anderen Zugang ebenfalls das Entscheidbarkeitsresultat von Weil und Kufleitner beweisen. Anstelle von sogenannten Rankern basiert ihre Charakterisierung auf Blockprodukten. In dieser Arbeit wird diese Technik auf die positive Alternierungshierarchie übertragen. Es werden verschiedene, auf Blockprodukten basierende, algebraische Charakterisierungen der Level der positiven Alternierungshierarchie vorgestellt und deren Entscheidbarkeit bewiesen.