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.