Vorlesung: Mi 12-14, SR11
In der Vorlesung werden formale Beweissysteme theoretisch behandelt. Grob gesagt hat eine formale Sprache ein effizientes Beweissystem, wenn man einen effizienten Verifizierer angeben kann, so dass für Worte in der Sprache mindestens ein Beweis vom Verifizierer akzeptiert wird, während für Worte ausserhalb der Sprache alle „Beweise“ verworfen werden. Wir betrachten verschiedene Varianten mit probabilistischen Verifizierern, Interaktion zwischen Beweiser und Verifizierer, mehreren unabhängigen Beweisern usw. Insbesondere das PCP Theorem, das beschreibt, wie für alle Sprachen in NP Beweise polynomieller Länge angegeben werden können, die durch Prüfen von nur konstant vielen Bits mit hoher Wahrscheinlichkeit zu verifizieren sind. Dieses Theorem hat viele Anwendungen in der Theorie der Approximationsalgorithmen.
[Weiterhin untersuchen wir Zero-Knowledge Beweise, die keine Information außer der Gültigkeit der bewiesenen Behauptung an den Verifizierer weitergeben. Im dritten Teil betrachten wir konkrete eingeschränkte Beweissysteme wie den Resolutionskalkül und zeigen untere Schranken für die Länge von Beweisen in solchen Systemen.]
Theorie formaler Beweissysteme:
Nichtdeterministische Berechnungen als Beweise
Probabilistische Beweissysteme: Arthur Merlin Spiele, allgemeine probabilistische Beweise und Zusammenhang zu platzbeschränkten Berechnungen, Systeme mit mehreren Beweisern, PCPs
Anwendungen: Schwierigkeit von Approximationsproblemen
Vordiplom Informatik erwünscht
Fachgespräch
18.10. .pps
.pdf
.ps
[Aussagenlogik, Resolution, NP und Beweissysteme, Beweise für Tautologien, Interaktion,
Graph Nichtisomorphismus]
25.10. .pps
.pdf
.ps
[Protokoll für quadratische Nichtreste, PSPACE, polynomielle Hierarchie]
1.11. .pps
.pdf
.ps
[PSPACE Vollständigkeit von QBF, AM und MA Definitionen]
8.11. .pps
.pdf
.ps
[TAUT und AM, Kollaps der AM-Hierarchie,IP]
15.11. .pps
.pdf
.ps
[AM und einseitiger Fehler, AM vs. IP, Graph-Nichtisomorphismus in AM]
22.11. .pps
.pdf
.ps
[TAUT in IP, IP und PSPACE]
29.11. .pps
.pdf
.ps
[IP=PSPACE]
6.12. .pps
.pdf
.ps
[MIP, PCPs, PCP und NTIME, PCP und MIP]
13.12. .pps
.pdf
.ps
[MIP mit 1 Runde, NEXP-Vollständigkeit]
20.12. .pps
.pdf
.ps
[Orakel-SAT NEXP vollst., MIP Protokoll für Orakel-SAT]
10.1. .pps
.pdf
.ps
[MIP Protokoll für Orakel-SAT, Multilinearitätstest]
17.1. .pps
.pdf
.ps
[NP in PCP(poly,O(1)): Hadamard Codes, lokale Dekodierung, QUADEQ NP-vollst.]
24.1. .pps
.pdf
.ps
[NP in PCP(poly,O(1)), Approximation und PCP]
31.1. .pps
.pdf
.ps
[Approximation und PCP, Kein Approximationsschema für Max-3-SAT, L-Reduktionen]
Übungsblätter:
25.10. .ps
1.11. .ps
8.11. .ps
22.11. .ps
29.11. .ps
6.12. .ps
20.12. .ps
Literatur:
Vadhan:
Lecture Notes on Probabilistic Proofs
Arora,
Barak: Interaktive Beweise
Trevisan: IP vs. PSPACE lecture
Arora,
Barak: PCP Theorem
Beame:
Proof Complexity
Arthur Merlin comic
31.1.2007 Hartmut Klauck