Algorithmisches Beweisen (Vorlesung)

Repetitorium zur Prüfungsvorbereitung am Freitag, den 19.02.2021, um 12:15 Uhr über BBB

Um einen Prüfungstermin zu bekommen, melden Sie sich per E-Mail mit Ihrer Matrikelnummer bei Frau Blaser:
silvia.blaser@uni-jena.de

Folien zu dieser Vorlesung finden Sie hier.

Modultitel (deutsch)

Algorithmisches Beweisen

Modultitel (englisch)

Proof Complexity and Solving

Modul-Verantwortliche/r

Olaf Beyersdorff

Empfohlene bzw. erwartete Vorkenntnisse

FMI-IN0001 Algorithmen und Datenstrukturen

FMI-IN0005 Automaten und Berechenbarkeit

Art des Moduls (Pflicht-, Wahlpflicht- oder Wahlmodul)

Wahlpflichtmodul (TIA, ALG) für den M.Sc. Informatik

Wahlpflichtmodul für den B.Sc. Informatik

Wahlpflichtmodul (Bereich Informatik) für den M.Sc. Bioinformatik

Wahlpflichtmodul (Angewandte Mathematik, Vertiefung Algorithmik, Nebenfach Informatik) für den M.Sc. Mathematik

Wahlpflichtmodul (Nebenfach Informatik) für den B.Sc. Mathematik

Wahlpflichtmodul für den B.Sc. Wirtschaftswissenschaften, Schwerpunkt IMS

Wahlpflichtmodul für den B.A. Ergänzungsfach Informatik

Dauer des Moduls

1 Semester

Zusammensetzung des Moduls / Lehrformen  (V, Ü, S, Praktikum, …)

4 V

Leistungspunkte (ECTS credits)

6 LP

Inhalte

Einführung in die Beweiskomplexität und algorithmische Aspekte von SAT mit den Themen:

  • Wichtige Beweissysteme
  • Harte Formeln für Resolution
  • Spieltechniken für untere Schranken
  • Algorithmen für Spezialfälle (Hornformeln, 2-SAT)
  • DPLL und CDCL Algorithmen
  • Zusammenhang zwischen Beweissystemen und SAT-Solvern
  • Geometrische und algebraische Beweissysteme
  • Frege-Kalküle
  • Quantifizierte Boolesche Formeln
  • Beweissysteme für modale Logik
  • Lokale Suchalgorithmen

Termine

Di. + Do., 12:00 – 14:00 Uhr

Lern- und Qualifikationsziele

Vertiefte Kenntnisse in Theoretischer Informatik, Logik und der algorithmischen Lösung von Erfüllbarkeitsproblemen.

Befähigung zur beweistheoretischen Einordnung konkreter Formelklassen

Kenntnisse über Techniken zum Nachweis unterer Schranken

Einsichten in Chancen und Grenzen moderner SAT-Solver

Empfohlene Literatur

Uwe Schöning, Jacobo Toran: Das Erfüllbarkeitsproblem SAT, Lehmanns 2012

Jan Krajicek: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press, 1995

Stasys Jukna: Boolean Function Complexity, Springer 2012