QBF-Beweise und Zertifikate

Mathematische Theoreme wie der Satz von Pythagoras oder der große Fermatsche Satz sind vielen Menschen geläufig. Mathematiker werden nicht nur dafür bewundert, diese Theoreme entdeckt zu haben, sondern auch für die Beweise, die diese Resultate untermauern. Ein Beweis garantiert die dauerhafte Gültigkeit eines Theorems, völlig unabhängig von künftigen Fortschritten in der Mathematik. Beweise haben in der Mathematik schon immer eine wichtige Rolle gespielt, genauso wie Zahlen, Funktionen, oder Gleichungen. Aber erst seit dem 20. Jahrhundert werden Beweise als eigenständige mathematische Objekte untersucht, wie etwa in den Arbeiten des österreichischen Logikers Kurt Gödel. Heute werden Beweise nicht nur in einem eigenen Zweig der mathematischen Logi k, der sogenannten Beweistheorie, und der philosophischen Logik untersucht, sondern auch in der Informatik. Dort garantieren Beweise die Sicherheit von Online-Zahlungsverfahren, Hardwaresystemen, sowie kryptografischen Protokollen. Im Zusammenhang mit Computern kann man sich Beweise als Zertifikate von wahren (1) und falschen (0) logischen Aussagen vorstellen, die die Korrekheit von Rechenergebnissen bestätigen, die ebenfalls als Folgen von Nullen und Einsen dargestellt werden. Wir möchten Beweise möglichst kurz halten, damit sie effizient übertragen werden können. Damit kommen wir zur zentralen Frage unserer Forschung: wie kurz kann ein Beweis sein? Die Größe eines Beweises entspricht der Anzahl von Bits in seiner Binärdarstellung. Die Beweisgröße hängt natürlich von der bewiesenen Aussage ab: je länger und komplizierter die Aussage, desto länger ist im Normalfall der Beweis. Aber um wieviel länger? Wenn die Beweisgröße exponentiell mit der Länge der Aussage wächst, werden Beweise für Anwendungen schnell zu groß. Das Gebiet der Beweiskomplexität beschäftigt sich mit solchen Fragen. Gegenstand dieses Forschungsprojekts ist eine Logik, die sich besonders gut dafür eignet, schwierige rechnerische Probleme als logische Probleme auszudrücken: die quantifizierte Aussagenlogik (engl. Quantified Boolean Formulas, kurz QBF). Das Ziel ist, kürzere QBF - Beweise für eine Reihe von Anwendungen zu ermöglichen. Wir orientieren uns dabei an neuesten Fortschritten beim automatisierten Lösen von QBFs, die wir um robuste Verfah ren zur Verifizierung von Lösungen erweitern wollen. Unser Vorhaben bewegt sich zwischen angewandter Forschung rund um das Lösen von QBFs, und theoretischer Forschung im Bereich der Beweistheorie. Wir erwarten, dass das Projekt neue Ergebnisse in diesen beiden Forschungszweigen nach sich ziehen wird.