Die Beweiskomplexität (engl. propositional proof complexity) ist ein Forschungsgebiet innerhalb der theoretischen Informatik, das die Länge von Beweisen in aussagenlogischen Beweissystemen untersucht. Der Forschungszweig entstand aus der Frage heraus, ob die Klasse NP aller Entscheidungsprobleme mit Beweisen polynomieller Länge unter Komplement abgeschlossen ist (NP vs. co-NP Problem) und befasst sich heutzutage hauptsächlich mit der Verbindung zwischen Beweissystemen und Algorithmen für NP-schwere Probleme. Bekanntestes Beispiel hierfür ist der Resolutionskalkül, welcher die Grundlage für nahezu alle modernen SAT-Solver bildet.
Die Lehrveranstaltung bietet eine Einführung in das Forschungsgebiet und seine Methoden. Einen besonderen Schwerpunkt bilden hierbei die vielfältigen Verbindungen zu benachbarten Gebieten, wie der Logik, der künstlichen Intelligenz und der linearen Optimierung. |
