Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Komplexität und Kryptografie

Seminar: Komplexität und Kryptologie

Dozent: Dr. Olaf Beyersdorff


Termin: SE Di 15-17 (RUD 26, 1'308) Dr. O. Beyersdorff

Zuordnung: Hauptstudium, Seminar

Inhalte und Lernziele


Im Zentrum dieses Seminars stehen aktuelle Themen zum algorithmischen Beweisen sowie der Beweiskomplexität. Einführend werden zunächst wichtige aussagenlogische Beweissysteme vorgestellt, wie z.B. das Resolutionssystem und seine Varianten, das Cutting-Planes-System sowie Frege-Systeme.
Im weiteren Seminarverlauf wollen wir uns dann schwerpunktmäßig mit den folgenden beiden Fragestellungen beschäftigen:

  1. Wie schwierig ist es, aussagenlogische Beweise zu konstruieren?  Diese Frage ist von großem praktischen Interesse und führt in das Gebiet des AutomatischenTheorembeweisens.
  2. Wie lang müssen aussagenlogische Beweise sein? Diese Frage ist aus komplexitätstheoretischem Blickwinkel interessant, da die minimale Beweislänge für aussagenlogsche Tautologien eng mit Fragen der Komplexitätstheorie wie dem P/NP-Problem zusammenhängt.

Das Seminar eignet sich gut zur Vorbereitung von Studien- oder Diplomarbeiten. Hörerwünsche bzgl. der Themengestaltung können berücksichtigt werden.


In den Vorträgen behandelte Themenbereiche



Termin Thema Vortragender
17.04. Themenvergabe Olaf Beyersdorff
08.05. Aussagenlogische Beweissysteme, das NP/coNP Problem, Resolution Oliver Kintzer
15.05. / 05.06.
Untere Schranken für die Beweislänge im Resolutionskalkül Nikolay Damyanliev

Algebraische und geometrische Beweissysteme Glenn Schütze

Automatisierbarkeit von Beweissystemen Andreas Kühnert




Empfohlene Literatur


  • M. Alekhnovich and A. A. Razborov. Resolution is not automatizable unless W[P] is tractable. In Proc. 42nd IEEE Foundations of Computer Science, pages 210-219, 2001.
  • P. W. Beame and T. Pitassi. Propositional proof complexity: Past, present, and future. In G. Paun, G. Rozenberg, and A. Salomaa, editors,Current Trends in Theoretical Computer Science: Entering the 21st Century, pages 42-70. World Scientific Publishing, 2001.
  • E. Ben-Sasson and A. Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001.
  • O. Beyersdorff. Disjoint NP-Pairs and Propositional Proof Systems. PhD thesis, Humboldt-Universität zu Berlin, 2006.
  • M. L. Bonet, T. Pitassi, and R. Raz. On interpolation and automatization for Frege systems. SIAM Journal on Computing, 29(6):1939-1967, 2000.
  • S. R. Buss. An introduction to proof theory. In S. R. Buss, editor, Handbook of Proof Theory, pages 1-78. Elsevier, Amsterdam, 1998.
  • C. Glaßer, A. L. Selman, and L. Zhang. Survey of disjoint NP-pairs and relations to propositional proof systems. In O. Goldreich, A. L. Rosenberg, and A. L. Selman, editors, Essays in Theoretical Computer Science in Memory of Shimon Even, pages 241-253. Springer-Verlag, Berlin Heidelberg, 2006.
  • H. Kleine Böning and T. Lettmann.Aussagenlogik: Deduktion und Algorithmen. B. G. Teubner, 1994.
  • J. Köbler, J. Messner, and J. Toran. Optimal proof systems imply complete sets for promise classes. Information and Computation, 184:71-92, 2003.
  • J. Krajicek. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995.
  • J. Krajicek. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997.
  • P. Pudlak. The lengths of proofs.In S. R. Buss, editor, Handbook of Proof Theory,pages 547-637. Elsevier, Amsterdam, 1998.
  • P. Pudlak. Proofs as games.American Math. Monthly, pages 541-550, 2000.
  • P. Pudlak. On reducibility and symmetry of disjoint NP-pairs.Theoretical Computer Science, 295:323-339, 2003.
  • P. Pudlak. Quantum deduction rules. Technical Report TR07-032, Electronic Colloquium on Computational Complexity, 2007.
  • U. Schöning. Perlen der Theoretischen Informatik. B. , I.-Wissenschaftsverlag, 1995.