Talk:
Complexity of Propositional Proofs:
Some Theory and Examples
Barcelona, April 29, 2015
Swansea, March 2015
Download talk slides: PDF
Abstract
We discuss the problem of separating Frege and extended
Frege proof systems. These are "textbook" proof systems
for propositional logic based on modus ponens as the only rule
of inference. Open questions about these systems are closely related
to problems in computational complexity about formula and circuit complexity,
as well to problems in proof search. Recent results by
several researchers have given a number of unexpected examples
of short Frege proofs. This includes new Frege proofs of
the pigeonhole principle (!) and a generalization known
as the Kneser-Lovasz coloring principle, new proofs of Frankl's theorem,
and new proofs of matrix identities.
The new Kneser-Lovasz proof is direct and simple, and
avoids the combinatorial algebraic geometry implicit in prior proofs.
This talk will provide an introduction to Frege proofs
and their complexity, and the new proofs of the pigeonhole principle
and the Kneser-Lovasz theorem which can be formalized as short
(quasipolynomial size)Frege proofs.
Part of this is joint work with James Aisenberg and Maria Luisa Bonet.