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

Die aussagenlogische Beweiskomplexitat ist ein aktives Forschungsgebiet im Schnittpunkt von Komplexitätstheorie und Logik mit wichtigen Anwendungen in der künstlichen Intelligenz. Dabei wurden vor allem schwache Beweissysteme wie Resolution intensiv untersucht, während fur starke Beweissysteme wie Frege-Systeme relativ wenig bekannt ist. Mit diesem Projekt wollen wir die Entwicklung einer allgemeinen Theorie zu starken Beweissystemen weiter vorantreiben. 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. Unsere Hauptziele in diesem Projekt 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 Lgik untersuchen wollen.

• DFG Programme: Research Grants
• Participating Person: Professor Dr. Olaf Beyersdorff