Linear equation systems and the search for a logical characterisation of polynomial time

Pakusa, Wied; Grädel, Erich (Thesis advisor); Otto, Martin (Thesis advisor); Dawar, Anuj (Thesis advisor)

Aachen (2015, 2016) [Doktorarbeit]

Seite(n): 1 Online-Ressource (vi, 173 Seiten) : Diagramme

Kurzfassung

Die Suche nach einer Logik für Polynomialzeit ist eines der wichtigsten offenen Probleme im Gebiet der Endlichen Modelltheorie.In den letzten Jahren wurden neue Erkenntnisse erzielt durch die Analyse der deskriptiven Komplexität von Problemen aus der (Linearen) Algebra. Gestartet wurden diese Untersuchungen 2007 nach einem Resultat von Atserias, Bulatov und Dawar welches zeigt, dass Fixpunktlogik mit Zählen (FPC) die Lösbarkeit linearer Gleichungssysteme über endlichen Abelschen Gruppen nicht ausdrücken kann. Dieses Ergebnis führte nicht zuletzt zur Definition neuer Kandidaten von Logiken für Polynomialzeit, zum Beispiel von Ranglogik (FPR), welche 2009 von Dawar, Grohe, Holm und Laubner eingeführt wurde. Ein weiterer wichtiger Kandidat ist Choiceless Polynomial Time (CPT), eine Logik die bereits 1999 von Blass, Gurevich und Shelah vorgeschlagen wurde. Diese Arbeit setzt die Suche nach einer Logik für Polynomialzeit fort, geleitet durch die folgenden Fragen. (I) Wie repräsentiert man algorithmische Techniken zum Lösen linearer Gleichungssysteme durch logische Mechanismen (Quantoren, Operatoren)?(II) Auf welchen Strukturklassen kann das Lösbarkeitsproblem für lineare Gleichungssysteme genutzt werden, um Polynomialzeit einzufangen? Zu (I) betrachten wir in Kapitel 3 das Lösbarkeitsproblem für lineare Gleichungssysteme über endlichen Abelschen Gruppen, Ringen und Moduln. Unser Ziel ist die Reduktion auf einfache Bereiche, z.B. auf Körper oder zyklische Gruppen, wobei die Transformationen in Fixpunktlogik definierbar sein soll. Wir zeigen, dass eine Reduktion auf zyklische Gruppen möglich ist für Gleichungssysteme über geordneten Gruppen, Ringen und Moduln, und auch für Systeme über gewissen Klassen kommutativer Ringe. In Kapitel 4 betrachten wir Ranglogik, das heißt die Erweiterung von FPC um Operatoren, die den Rang von Matrizen über endlichen Körper definieren. Unser Hauptergebnis bestätigt eine Vermutung von Dawar und Holm: Rangoperatoren über verschiedenen Primkörpern haben unterschiedliche Ausdrucksstärke. Eine wichtige Folgerung ist, dass Ranglogik, in der ursprünglichen Definition mit einem separaten Rangoperator für jede Primzahl, nicht Polynomialzeit einfängt, und durch die stärkere Logik mit uniformem Rangoperator ersetzt werden sollte.Weiter zeigen wir, dass, ohne Hinzunahme von Zähloperatoren, Matrizenrang nicht durch entsprechende Lösbarkeitsquantoren ausgedrückt werden kann. Zu (II) führen wir in 5 zyklische lineare Gleichungssysteme ein. Solche System sind strukturell einfach, aber dennoch stark genung, um das Cai, Fürer, Immerman Problem zu kodieren, und damit um FPC von Polynomialzeit zu trennen. Unser Hauptergebnis ist, dass CPT die Lösbarkeit zyklischer Gleichungssysteme ausdrücken kann.In Kapitel 6 benutzen wir dieses Resultat um zu zeigen, dass CPT Polynomialzeit einfängt auf Strukturen mit Abelschen Farben. Dieses Ergebnis löst auch ein offenes Problem von Blass, Gurevich und Shelah: das Isomorphieproblem von multipedes ist definierbar in CPT.

Identifikationsnummern

  • URN: urn:nbn:de:hbz:82-rwth-2016-008390
  • REPORT NUMBER: RWTH-2016-00839