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:
- Wie schwierig ist es, aussagenlogische Beweise zu konstruieren? Diese Frage ist von großem praktischen Interesse und führt in das Gebiet des AutomatischenTheorembeweisens.
- 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.