Vorlesung

Beweissysteme

Hartmut Klauck

WS 2006/07

 

Termine:

Vorlesung: Mi 12-14, SR11

 

Inhalt:

 

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

 

 

Vorkenntnisse:

Vordiplom Informatik erwünscht

Scheinerwerb:

Fachgespräch


Vorlesungen:

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