Termine: | VL Do 15 - 17 (Rud. 3.101) J. Köbler und O. Beyersdorff |
---|
Zuordnung: | Hauptstudium, Halbkurs (2. Teil) |
---|
Die Aussagenlogik und deren Beweiskalküle sind grundlegend
für die theoretische Informatik und finden unter anderem in Form von
Thereombeweisern vielfältige Anwendungen.
In der Vorlesung werden verschiedene aussagenlogische Beweissysteme
vorgestellt. Zentral ist die Untersuchung der Beweislänge aussagenlogischer
Tautologien: Gibt es ein Beweissystem, in dem alle Tautologien Beweise
polynomieller Länge besitzen? Eine negative Antwort auf diese Frage
impliziert die Separierung der Komplexitätsklassen NP und coNP, und
damit die Lösung des P/NP-Problems.
Für spezielle Beweissysteme werden exponentielle untere Schranken
für die Beweislänge gezeigt.
Die Vorlesung schließt an die gleichnamige Veranstaltung des Wintersemesters an, kann jedoch auch unabhängig davon besucht werden.
Die VL kann sowohl mit der VL "Algorithmisches Beweisen" aus dem WS
01/02 als auch mit der VL "Komplexität boolescher Funktionen" zu einem
Halbkurs kombiniert werden.
[1] | S. R. Buss (ed.), Handbook of Proof Theory, North-Holland, 1999. |
[2] | S.R. Buss, Propositional Proof Complexity, An Introduction. |
[3] | P. Beame, T. Pitassi, Propositional Proof Complexity. Past, Present, and Future. |
[4] | E. Ben-Sasson, A. Wigderson, Short Proofs are Narrow - Resolution made Simple. Proc. of the 31st ACM STOC, p. 517-526, 1999. |
[5] | H. Kleine Büning, T. Lettmann, Aussagenlogik: Deduktion und Algorithmen, Teubner, 1994 |
[6] | J. Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995. |