Formale Analyse von Wahlverfahren

Formale Analyse von Wahlverfahren
Veranstaltungstyp: Proseminar
Veranstaltungsnr.: WS132400022
Zielgruppe: Bachelor Informatik
Lehrstuhl: Anwendungsorientierte Formale Verifikation; Logik und Formale Methoden
Dozierende:

Prof. B. Beckert
Prof. P. H. Schmitt

SWS-Anzahl: 2
ECTS: 3
Semester: Wintersemester 2013/14
Raum: wird hier rechtzeitig bekanntgegeben
Termine: Mi., 23.10.2013, 13:00, Auftaktveranstaltung
(weitere Termine nach Vereinbarung)
Anmeldung: Bei Frau Meinhart, Raum 223, simone.meinhart@kit.edu

Thema

Das Urteil des Bundesverfassungsgericht vom 3. Juli 2008 stellt fest, dass der Effekt des negativen Stimmgewichts die Grundsätze der Gleichheit und Unmittelbarkeit der Wahl verletzt. Der Gesetzgeber wurde verpflichtet, das im Bundeswahlgesetz geregelte Wahlverfahren zu verbessern.

  • Warum ist es eigentlich so schwer ein faires Wahlverfahren zu entwerfen?
  • Wann nennen wir ein Wahlverfahren fair?
  • Welche Eigenschaften sollte ein Wahlverfahren überhaupt haben?
  • Kann man formal verifizieren, dass ein vorgeschlagenes Wahlverfahren keine paradoxen Eigenschaften hat?

Computer spielen eine immer größere Rolle bei der Durchführung von Wahlen. Im Blick der Öffentlichkeit steht dabei hauptsächlich der Einsatz von Computern zur Modernisierung und Verbesserung der Stimmabgabe und administrativer Prozesse wie der Wählerregistrierung. Computer kommen aber auch bei der Umsetzung des eigentlichen Wahlverfahrens zum Einsatz, bei der Berechnung des Wahlergebnisses aus den abgegebenen Stimmen. Und gerade auch bei diesem essentiellen Kern einer Wahl ermöglichen Computer Verbesserung, führen aber auch zu neuen Problemen. Die Frage, wie man mit Informatik-Methoden dafür sorgen kann, dass die Verbesserungen überwiegen, macht Wahlverfahren zu einem hochinteressanten und bedeutenden Informatik-Thema.

Vorträge

  1. Es wird allen Vortragenden empfohlen sich Kapitel 1 von [HK05] als Hintergrundinformation durchzulesen. Hierzu ist kein Vortrag vorgesehen.
  2. Grundlegende Begriffee. Kapitel 2 und 3 aus [HK05].
  3. Das Theorem von Arrow. Wie fair kann ein Wahlverfahren sein? (Kapitel 4 und 5 aus [HK05].)
  4. Gewichtete Abstimmungen. (Kapitel 6 aus [HK05].)
  5. Referendum. Probleme mit der direkten Demokratie. (Kapitel 9 aus [HK05].)
  6. Proportionale Aufteilung. (Kapitel 10 aus [HK05].)
  7. Das "negative Stimmgewicht" bei Bundestagswahlen
  8. Manipulierbarkeit von Wahlen. Das Theorem von Gibbard-Satterthwaite. (Abschnitt 2.3 in [Endriss11])
  9. Blacks Theorem: Median Voter Rule
  10. Formalisierung der Eigenschaften von Wahlverfahren in Prädikatenlogik am Beispiel von "Single Transferable Vote"
  11. Single Transferable Vote: Probleme im Wahlverfahren der CADE Trustee Elections

Literatur:

[HK05]
The Mathematics of Voting and Elections: A Hands-On Approach
Jonathan K. Hodge, Richard E Klima
Mathematical World, Vol. 22
Published by AMS, 2005
Das Buch ist in der Informatikbibliothek vorhanden.
Beachten Sie auch die Fehlerkorrektur dazu.

[Endriss11]
Ulle Endriss.
Logic and Social Choice Theory.
In A. Gupta and J. van Benthem, editors, Logic and Philosophy Today, volume 2, pages 333-377, College Publications, 2011 PDF

[BGS13]
Bernhard Beckert, Rajeev Gore, and Carsten Schürmann. On the Specification and Verification of Voting Schemes. In 4th International Conference on E-Voting and Identity, Vote-ID 2013, LNCS 7985. PDF

Aufgabenstellung

Für jeden Vortrag sind von den Studierenden die folgenden Aufgabenpunkte zu erledigen:

  • Verstehen des Stoffes.
  • Auswahl der Themen, die in dem Vortrag präsentiert werden sollen.
  • Entscheidung wie, die Themen präsentiert werden sollen.
  • Erstellung der Folien für die Präsentation und gegebenfalls anderer Materialien.
  • Der Vortrag selbst.