Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Komplexität und Kryptografie

Aussagenlogische Beweiskomplexität und disjunkte NP-Paare (2)

DFG Forschungsprojekt


Das Projekt wird von der Deutschen Forschungsgemeinschaft (DFG) gefördert.

Zeitraum: April 2008 bis März 2010


Projektmitglieder:  Johannes Köbler, Olaf Beyersdorff, Sebastian Müller


Forschungsinhalt


Zur Analyse aussagenlogischer Beweissysteme wurden in den letzten Jahren neben logischen zunehmend kombinatorische, kryptografische und komplexitätstheoretische Techniken herangezogen, die neue Sichtweisen auf beweistheoretische Fragen eröffnen. Unter Ausnutzung dieser Techniken wollen wir im Projekt die Entwicklung einer allgemeinen Theorie zu Beweissystemen weiter vorantreiben. Dabei konzentrieren wir uns auf starke Beweissysteme wie Frege-Systeme, zu denen im Vergleich zu schwachen Systemen wie Resolution viele Fragen noch ungeklärt sind. Als ausdrucksstarkes Werkzeug haben sich hierbei im bisherigen Projektverlauf disjunkte NP-Paare erwiesen.

Ein Schwerpunkt dieses Projektes liegt auf der Untersuchung charakteristischer Eigenschaften praktisch wichtiger Beweissysteme. Diese Eigenschaften wollen wir mit Hilfe disjunkter NP-Paare modellieren und im Verband der NP-Paare komplexitätstheoretisch analysieren. Ein weiteres Ziel ist der Einsatz kryptografischer Konzepte wie Pseudozufallsgeneratoren zum Nachweis unterer Schranken für die Beweislänge. Das Fernziel sind hier untere Schranken für erweiterte Frege Systeme. Auch zur Analyse solcher kryptografischen Annahmen wollen wir disjunkte NP-Paare einsetzen.