Aussagenlogische Beweiskomplexität und disjunkte NP-Paare

• Antragsteller: Professor Dr. Johannes Köbler
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2005 bis 2010
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Olaf Beyersdorff