Complexity of propositional proofs: some theory and examples.

Samuel Buss

(University of California)

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.
Thursday 26th March 2015, 14:00
Robert Recorde Room
Department of Computer Science