Humboldt-Universität zu Berlin, Institut für Informatik

Lehrstuhl für Komplexität und Kryptografie

Vorlesung:  Algorithmisches Beweisen

Dozent: Prof. Johannes Köbler und Olaf Beyersdorff
Termine: VL  Do 15 - 17  (Rud. 3.101)    J. Köbler und O. Beyersdorff 
 
  Verlegt auf Do 11-13 (Rud. 4.110)
Zuordnung: Hauptstudium, Halbkurs (2. Teil)

Inhalte und Lernziele


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.
 
 


Literatur

[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.