# Seminar Logic, Complexity, Games: Propositional Proof Complexity

## WS 2022/23

### News

- Kickoff meeting and topic selection: TBA

### Registration

- Students with a subject in mathematics can apply by writing an email to seminar [AT] logic.rwth-aachen.de including their name, immatriculation no., subject of studies, no. of semesters of studies, and information about relevant modules they have passed (especially lectures from our group).
- Students with a subject in computer science can register via the SuPra website.

### Organisation

The presentations will take place as a block seminar at the end of the semester. Presentations may be held in either English or German.- Length of seminar papers: TBD, around 5-6 pages.
- Duration of presentations: 25 minutes.

### Content

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.

### Introductory Literature

We recommend the following survey article as an introduction to proof coplexity: [BeamePitassi01]

### Topics

TBA### Literature

[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. |

### Classification

- Bachelor Informatik
- Master Informatik
- Bachelor Lehramt Informatik
- Master Lehramt Informatik
- Bachelor Mathematik
- Master Mathematik

### Prerequisites

- Mathematical Logic
- for B.Sc. Computer Science: Module "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

### Contact

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