Aussagenlogische Beweiskomplexität und disjunkte NP-Paare
DFG Forschungsprojekt
Das Projekt wird von der Deutschen Forschungsgemeinschaft (DFG) gefördert.
Zeitraum: April 2006 bis März 2008
Projektmitglieder: Johannes Köbler, Olaf Beyersdorff
Forschungsinhalt
Die aussagenlogische Beweiskomplexität ist ein aktives
Forschungsgebiet im Schnittpunkt von Komplexitätstheorie und Logik mit
wichtigen Anwendungen in der künstlichen Intelligenz. Bislang hat sich
die Forschung dabei vor allem auf schwache Beweissysteme wie Resolution
konzentriert, während für starke Beweissysteme wie Frege-Systeme
relativ wenig bekannt ist. Ein zentrales Anliegen dieses Projekts ist
daher die Entwicklung einer allgemeinen Theorie zu starken
Beweissystemen. Dazu wollen wir neue Ansätze aus der
Komplexitätstheorie, Kryptografie und Logik kombinieren, bezüglich
derer in den letzten Jahren beachtliche Fortschritte erzielt wurden. Im
einzelnen sind dies:
- die Verwendung von Pseudozufallsgeneratoren in der
Beweistheorie,
- die Untersuchung des Verbands disjunkter NP-Paare und
- die Beziehung von Beweissystemen zur beschränkten Arithmetik.
Hauptziele des Projekts sind der Nachweis unterer Schranken für die Beweislänge in starken Beweissystemen unter Benutzung kryptografischer und komplexitätstheoretischer Härtevoraussetzungen und die Charakterisierung von Beweissystemen im Verband disjunkter NP-Paare, den wir mit Methoden der Logik untersuchen.