Seminar Logik, Komplexität, Spiele: Beweiskomplexität

WS 2022/23

Aktuelles

  • Vorbesprechung und Themenvergabe: TBA

Anmeldung

  • Studierende in Mathematik-Studiengängen können sich per Email an seminar [AT] logic.rwth-aachen.de bewerben. Bitte geben Sie dazu Ihren vollständigen Namen, Matrikelnummer, Studiengang, Fachsemester und Ihre Vorkenntnisse (insbesondere an unserem Lehrgebiet besuchte Vorlesungen) an.
  • Studierende in Informatik-Studiengängen können sich über die zentrale Vergabe von Seminarplätzen bewerben.

Organisation

Die Veranstaltung wird als Blockseminar angeboten. Die Vorträge werden am Ende des Semesters wahlweise auf deutsch oder englisch gehalten.
  • Länge der Ausarbeitung: TBD, etwa 5-6 Seiten.
  • Vortragsdauer: 25 Minuten.

Inhalt

Propositional proof complexity is the study of syntactical logical proof systems and their power. Standard examples of such systems, that are introduced in the course „Mathematische Logik“, are resolution and the sequent calculus. Such proof systems typically allow to prove the unsatisfiability of a given propositional formula by means of syntactic inference rules. For instance, the empty clause is derivable from a formula in conjunctive normal form using the resolution rule if and only if the original formula is unsatisfiable. Such a derivation of the empty clause is called a refutation of the formula. Now when we study the complexity of a proof system such as resolution, the questions that arise are of this kind:

Are there unsatisfiable formulas that have no short refutations? If so, how large is a shortest refutation in the worst case? Which proof systems admit efficient algorithms for computing refutations?

For resolution, the first two questions were answered in 1984 by Armin Haken, who proved that a propositional formulation of the pigeonhole principle only admits super-polynomially large resolution refutations. Since then, a lot of effort has gone into proving such super-polynomial lower bounds for more efficient proof systems as well. In this seminar, we will in particular also cover lower bounds for algebraic proof systems such as the Polynomial Calculus or the Cutting Planes proof system, which manipulate equations rather than logical formulas. Research in proof complexity is motivated by several aspects: First of all, it has a connection to practical computer science, as many SAT solvers are based on formal proof systems. Thus, lower bounds from proof complexity also imply lower bounds for certain SAT solvers, and conversely, the discovery of efficient proof systems can inspire new SAT solving algorithms.

In this seminar, however, the focus is mostly on the impact for theoretical computer science: Proof complexity can in principle help to solve the open question whether NP equals co-NP. It is known that these classes are equal if and only if there exists a proof system that admits a polynomial-size refutation for every unsatisfiable formula. Thus, an approach to separate NP from co-NP (and thereby also P from NP) is to try and show that no such proof system exists. This long-term goal is one of the reasons for the interest in lower bounds for the various proof systems.

Einführungsliteratur

Folgender Übersichtsartikel ist für alle Themen als Einführungsliteratur empfohlen: [BeamePitassi01]

Themen

TBA

Literatur

[BeamePitassi01]P. Beame and T. Pitassi. Propositional Proof Complexity: Past, Present, and Future. In Current Trends in Theoretical Computer Science, Entering the 21th Century (G. Paun, G. Rozenberg, and A. Salomaa, Eds.), pp. 42–70. World Scientific, 2001.

Zuordnung

  • Bachelor Informatik
  • Master Informatik
  • Bachelor Lehramt Informatik
  • Master Lehramt Informatik
  • Bachelor Mathematik
  • Master Mathematik

Voraussetzungen

  • Mathematische Logik
  • für B.Sc. Informatik: bestandenes Modul "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Rückfragen

Erich Grädel, Benedikt Pago, Matthias Naaf, Lovro Mrkonjić