28. Januar – 02. Februar 2018, Dagstuhl Seminar 18051

Proof Complexity


Albert Atserias (UPC – Barcelona, ES)
Jakob Nordström (KTH Royal Institute of Technology – Stockholm, SE)
Pavel Pudlák (The Czech Academy of Sciences – Prague, CZ)
Rahul Santhanam (University of Oxford, GB)

Auskunft zu diesem Dagstuhl Seminar erteilen

Annette Beyer zu administrativen Fragen

Marc Herbstritt zu wissenschaftlichen Fragen


The study of proof complexity was initiated by Cook and Reckhow in 1979 as a way to attack the P vs. NP problem, and in the ensuing decades many powerful techniques have been discovered for understanding different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are when measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables.

During the last 10-15 years the area of proof complexity has seen a revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent progress gives hope that the area may be ripe for decisive breakthroughs.

In this Dagstuhl Seminar, we aim to bring together leading experts covering the whole spectrum of proof complexity from Frege proof systems and circuit-inspired lower bounds via geometric and algebraic proof systems all the way to bounded arithmetic, as well as prominent researchers from neighbouring fields. We hope and believe that such a seminar could have a major impact at this critical juncture. Besides the regular program including talks about recent research results, we plan to organize open problem sessions, and expect ongoing research discussions throughout the week in smaller groups.

  Creative Commons BY 3.0 DE
  Jakob Nordström and Pavel Pudlák and Rahul Santhanam


  • Data Structures / Algorithms / Complexity
  • Verification / Logic


  • Proof complexity
  • Computational complexity
  • Logic
  • Bounded arithmetic
  • Satisfiability algorithms


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.