Aussagenlogische Beweiskomplexität und disjunkte NP-Paare

• Applicant: Professor Dr. Johannes Köbler
• Subject Area: Theoretical Computer Science
• Term: from 2005 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 17136727

• Final Report Year: 2010

Final Report Abstract

Zentrales Anliegen des Projekts war das bessere Verständnis und der Aufbau einer allgemeinen Theorie für starke aussagenlogische Beweissysteme wie Frege-Systeme und deren Erweiterungen. Unsere Hauptbeiträge zu diesem Ziel bestehen in neuen Erkenntnissen zu folgenden Fragen: 1. Welche logischen Eigenschaften sind für starke Beweissysteme charakteristisch? 2. Gibt es ein optimales, d.h. ein stärkstes Beweissystem? 3. Lasst sich die Beweiskraft durch Hinzuziehen weiterer Rechenressourcen wie Advice verstärken? Als zentrale Werkzeuge fur die Beantwortung der ersten Frage haben sich disjunkte NP-Paare zu aussagenlogischen Beweissystemen und die Korrespondenz zur beschränkten Arithmetik erwiesen. Des Weiteren haben wir die Deduktionseigenschaft als eine charakteristische Eigenschaft fur Frege-Systeme und deren Erweiterungen identifiziert. Für die zweite Frage zeigen wir eine Reihe neuer Charakterisierungen und weisen einen engen Zusammenhang zu den im letzten Absatz angesprochenen Eigenschaften nach. Bleibt die Frage nach optimalen Beweissystemen im klassischen Modell offen, so erhalten wir positive Antworten in stärkeren Modellen, in denen die Beweissysteme zur Beweisverifikation auf Advice oder Orakel zugreifen konnen. Motiviert durch dieses Resultat untersuchen wir Beweissysteme mit Advice genauer: wir erhalten eine vollständige komplexitätstheoretische Charakterisierung für Sprachen mit polynomiell beschränkten Beweissystemen und analysieren Möglichkeiten zur Vereinfachung des für praktische Belange unrealistisch starken Advicemodells. Auch für Beweissysteme mit Advice bleibt die Korrespondenz zur beschränkten Arithmetik bestehen. Unter Benutzung dieses Zusammenhangs zeigen wir ein optimales Karp-Lipton-Kollapsresultat in beschränkter Arithmetik, womit wir ein von Cook und Krajicek gestelltes Problem lösen. Über diese Ergebnisse hinaus haben wir im Projektverlauf auch weiterführende Themen behandelt, die wir bei der Antragstellung noch nicht berücksichtigt hatten, sondern die sich zum Teil während des Projekts aus aktuellen Arbeiten anderer Forschergruppen ergeben haben. Dies betrifft unsere Untersuchungen zur parametrisierten Beweiskomplexität und zur Beweiskomplexität nichtklassischer Logiken. In der parametrisierten Beweiskomplexität konzentrieren wir uns auf parametrisierte Resolution, die sich im Gegensatz zur klassischen Resolution als relativ starkes Beweissystem erweist. Dies untermauern wir durch die Konstruktion kurzer Beweise für eine Reihe klassisch harter Formeln sowie durch Härteresultate für das Pigeonhole Principle, die wir mittels einer neuen Spiel-Technik erhalten. In nichtklassischer Beweiskomplexität untersuchen wir aussagenlogische Default-Logik und zeigen einen engen Zusammenhang zur beweistheoretischen Stärke von klassischen Frege-Systemen.

Publications

• Classes of representable disjoint NP-pairs. Theoretical Computer Science, 377:93-109, 2007
  O. Beyersdorff
  
• Tuples of disjoint NP-sets. Theory of Computing Systems, 43(2):118-135, 2008. (Special Edition der CSR'06)
  O. Beyersdorff
  
• Characterizing the existence of optimal proof systems and complete sets for promise classes. In Proc. 4th International Computer Science Symposium in Russia, Band 5675 der Lecture Notes in Computer Science, Seiten 47-58. Springer-Verlag, 2009
  O. Beyersdorff und Z. Sadowski.
  
• Nondeterministic functions and the existence of optimal proof systems. Theoretical Computer Science, 410(38-40):3839-3855, 2009
  O. Beyersdorff, J. Köbler und J. Messner
  
• On the correspondence between arithmetic theories and propositional proof systems - a survey. Mathematical Logic Quarterly, 55(2):116-137, 2009
  O. Beyersdorff
  
• On the existence of complete disjoint NP-pairs. In Proc. 11th International Symposium on Symbolic and Numeric Algorithms for Scientic Computing, Seiten 282-289. IEEE Computer Society Press, 2009
  O. Beyersdorff
  
• The complexity of propositional implication. Information Processing Letters, 109(18):1071-1077, 2009
  O. Beyersdorff, A. Meier, M. Thomas und H. Vollmer
  
• The complexity of reasoning for fragments of default logic. In Proc. 12th International Conference on Theory and Applications of Satisfiability Testing, Band 5584 der Lecture Notes in Computer Science, Seiten 51-64. Springer-Verlag, 2009
  O. Beyersdorff, A. Meier, M. Thomas und H. Vollmer
  
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Technischer Bericht TR10-081, Electronic Colloquium on Computational Complexity, 2010
  O. Beyersdorff, N. Galesi und M. Lauria
  
• A tight Karp-Lipton collapse result in bounded arithmetic. ACM Transactions on Computational Logic, 11(4), 2010. (Special Edition der CSL'08)
  O. Beyersdorff und S. Müller
  
• Different approaches to proof systems. In Proc. 7th Conference on Theory and Applications of Models of Computation. Band 6108 der Lecture Notes in Computer Science, Seiten 50-59. Springer-Verlag, 2010
  O. Beyersdorff und S. Müller
  
• Hardness of parameterized resolution. Technischer Bericht TR10-059, Electronic Colloquium on Computational Complexity, 2010
  O. Beyersdorff, N. Galesi und M. Lauria
  
• Proof complexity of non-classical logics. In Proc. 7th Conference on Theory and Applications of Models of Computation. Band 6108 der Lecture Notes in Computer Science, Seiten 15-27. Springer-Verlag, 2010
  O. Beyersdorff
  
• Proof complexity of propositional default logic. In Proc. 13th International Conference on Theory and Applications of Satisfiability Testing, Band 6175 der Lecture Notes in Computer Science, Seiten 30-43. Springer-Verlag, 2010
  O. Beyersdorff, A. Meier, S. Müller, M. Thomas und H. Vollmer
  
• The deduction theorem for strong propositional proof systems. Theory of Computing Systems, 47(1):162-178, 2010
  O. Beyersdorff