
×
Non-classical Aspects in Proof Complexity
von Olaf BeyersdorffProof complexity focuses on the complexity of theorem proving procedures, a
topic which is tightly linked to questions from computational complexity (the
separation of complexity classes), first-order arithmetic theories (bounded arithmetic),
and practical questions as automated theorem proving. One fascinating
question in proof complexity is whether powerful computational resources as randomness
or oracle access can shorten proofs or speed up proof search. In this
dissertation we investigated these questions for proof systems that use a limited
amount of non-uniform information (advice). This model is very interesting as---
in contrast to the classical setting---it admits an optimal proof system as recently
shown by Cook and Krajícek. We give a complete complexity-theoretic classification
of all languages admitting polynomially bounded proof systems with advice
and explore whether the advice can be simplified or even eliminated while still
preserving the power of the system.
Propositional proof systems enjoy a close connection to bounded arithmetic.
Cook and Krajícek (JSL'07) use the correspondence between proof systems with
advice and arithmetic theories to obtain a very strong Karp-Lipton collapse result
in bounded arithmetic: if SAT has polynomial-size Boolean circuits, then the
polynomial hierarchy collapses to the Boolean hierarchy. Here we show that this
collapse consequence is in fact optimal with respect to the theory PV, thereby
answering a question of Cook and Krajícek.
The second main topic of this dissertation is parameterized proof complexity, a
paradigm developed by Dantchev, Martin, and Szeider (FOCS'07) which transfers
the highly successful approach of parameterized complexity to the study of proof
lengths. In this thesis we introduce a powerful two player game to model and
study the complexity of proofs in a tree-like Resolution system in a setting arising
from parameterized complexity. This game is also applicable to show strong
lower bounds in other tree-like proof systems. Moreover, we obtain the first lower
bound to the general dag-like Parameterized Resolution system for the pigeonhole
principle and study a variant of the DPLL algorithm in the parameterized setting.
In der Beweiskomplexität steht die Komplexität des Theorembeweisens im Mittelpunkt, eine Frage, die eng mit zentralen Problemen der Komplexitätstheorie (der Trennung von Komplexitätsklassen), der erststufigen Logik (beschränkte Arithmetik) und praktischen Fragen wie dem automatisierten Theorembeweisen verknüpft ist. Eine faszinierende Frage in der Beweiskomplexität ist, ob es durch die Nutzung starker Berechnungsressourcen wie Randomisierung oder Orakelzugriff möglich wird, die Beweislängen zu verkürzen oder die Beweissuche zu beschleunigen. Hier untersuchen wir diese Fragen für Beweissysteme, die auf eine kleine Menge nichtuniformer Information (Advice) zugreifen können. Insbesondere erhalten wir eine vollständige komplexitätstheoretische Klassifikation aller Sprachen mit polynomiell beschränkten Beweissystemen mit Advice und analysieren Möglichkeiten zur Vereinfachung des für den praktischen Einsatz unrealistisch starken Advice- Modells. Eine wichtige Querverbindung führt von aussagenlogischen Beweissystemen in die erststufige Logik zur beschränkten Arithmetik. Mit Hilfe dieser Korrespondenz zeigen Cook und Krajícek (JSL'07) einen sehr starken Karp-Lipton Kollaps in der beschränkten Arithmetik. Hier zeigen wir, dass dieses Kollapsresultat in der Tat optimal bezüglich der Theorie PV ist, womit wir eine von Cook und Krajícek gestellte Frage beantworten. Der zweite nichtklassische Aspekt dieser Arbeit ist die Untersuchung parametrisierter Beweissysteme. Die parametrisierte Beweiskomplexität, entwickelt von Dantchev, Martin und Szeider (FOCS'07), überträgt den erfolgreichen Ansatz der parametrisierten Komplexität auf die Analyse von Beweislängen. Hier entwickeln wir ein 2-Personen-Spiel, mit dessen Hilfe wir Beweislängen in baumförmiger Resolution im parametrisierten Kontext abschätzen. Dieses Spiel liefert auch eine neue Technik zum Nachweis starker unterer Schranken in anderen baumförmigen Beweissystemen. Darüber hinaus zeigen wir für das Pigeonhole Principle die erste untere Schranke für allgemeine parametrisierte Resolution und untersuchen eine Variante des DPLL Algorithmus für parametrisierte Formeln.
In der Beweiskomplexität steht die Komplexität des Theorembeweisens im Mittelpunkt, eine Frage, die eng mit zentralen Problemen der Komplexitätstheorie (der Trennung von Komplexitätsklassen), der erststufigen Logik (beschränkte Arithmetik) und praktischen Fragen wie dem automatisierten Theorembeweisen verknüpft ist. Eine faszinierende Frage in der Beweiskomplexität ist, ob es durch die Nutzung starker Berechnungsressourcen wie Randomisierung oder Orakelzugriff möglich wird, die Beweislängen zu verkürzen oder die Beweissuche zu beschleunigen. Hier untersuchen wir diese Fragen für Beweissysteme, die auf eine kleine Menge nichtuniformer Information (Advice) zugreifen können. Insbesondere erhalten wir eine vollständige komplexitätstheoretische Klassifikation aller Sprachen mit polynomiell beschränkten Beweissystemen mit Advice und analysieren Möglichkeiten zur Vereinfachung des für den praktischen Einsatz unrealistisch starken Advice- Modells. Eine wichtige Querverbindung führt von aussagenlogischen Beweissystemen in die erststufige Logik zur beschränkten Arithmetik. Mit Hilfe dieser Korrespondenz zeigen Cook und Krajícek (JSL'07) einen sehr starken Karp-Lipton Kollaps in der beschränkten Arithmetik. Hier zeigen wir, dass dieses Kollapsresultat in der Tat optimal bezüglich der Theorie PV ist, womit wir eine von Cook und Krajícek gestellte Frage beantworten. Der zweite nichtklassische Aspekt dieser Arbeit ist die Untersuchung parametrisierter Beweissysteme. Die parametrisierte Beweiskomplexität, entwickelt von Dantchev, Martin und Szeider (FOCS'07), überträgt den erfolgreichen Ansatz der parametrisierten Komplexität auf die Analyse von Beweislängen. Hier entwickeln wir ein 2-Personen-Spiel, mit dessen Hilfe wir Beweislängen in baumförmiger Resolution im parametrisierten Kontext abschätzen. Dieses Spiel liefert auch eine neue Technik zum Nachweis starker unterer Schranken in anderen baumförmigen Beweissystemen. Darüber hinaus zeigen wir für das Pigeonhole Principle die erste untere Schranke für allgemeine parametrisierte Resolution und untersuchen eine Variante des DPLL Algorithmus für parametrisierte Formeln.