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

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.