New directions in proof complexity

Workshop theme

Proof complexity is an area of mathematics (and mathematical logic and computational complexity theory in particular) centered around the problem whether the complexity class NP is closed under complementation. With a suitable general definition of a propositional proof system (Cook and Reckhow 1979) this becomes a lengths-of-proofs question: Is there a propositional proof system in which every tautology admits a proof whose length is bounded above by a polynomial in the length of the tautology? The ultimate goal of proof complexity is to show that there is no such proof system; that is, to demonstrate superpolynomial lower bounds for all proof systems.

Strong lower bounds are known for some particular, classical proof systems. (In fact, also surprising upper bounds are known!) The methods used for proving these lower bounds borrow from all parts of logic, from finite combinatorics, from parts of complexity theory including circuit complexity, communication complexity, cryptography, derandomization, from classical algebra like field theory or representation theory, or from abstract concepts of geometry like Euler characteristic and Grothendieck ring.

The purpose of the conference is to bring together researchers in various parts of mathematics and computer science interested in proof complexity. Our ambition is to expose, through invited and contributed lectures, current developments in proof complexity as well as new ideas and directions of research pursued most recently.

Applications for this workshop are now closed

Timetable

Monday 10th April 2006
08:30 to 10:00	Registration	No Room Required
10:00 to 11:00	Pavel Pudlak $On \forall\Sigma_1^b$ sentences provable in bounded arithmetic	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	The complexity of proving the discrete Jordan Curve theorem and related principles	Room 1
12:00 to 12:30	Uniform proof complexity	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 15:00	Neil Thapen Charles University, Prague $T^1_2, T^2_2$ and search problems	Room 1
15:00 to 15:30	Tea	No Room Required
15:30 to 16:00	Emil Jerabek University of Toronto Approximate counting in bounded arithmetic	Room 1
16:00 to 16:30	Chris Pollett When can $S^1_2$ prove the weak pigeonhole principle?	Room 1
17:00 to 18:00	Wine and Beer Reception	No Room Required
18:45 to 19:30	Dinner at Wolfson Court (Residents only)	No Room Required

Tuesday 11th April 2006
09:30 to 10:30	Stephen Cook University of Toronto Capturing complexity classes by their reasoning power	Room 1
10:30 to 11:00	Moshe Vardi Rice University Constraint propagation as a proof system	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Michael Soltys McMaster University The proof complexity of matrix algebra	Room 1
12:00 to 12:30	Steven Perron University of Toronto A minimal quantified proof system for polytime reasoning	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 15:00	Russell Impagliazzo University of California Which SAT instances are the hardest?	Room 1
15:00 to 15:30	Tea	No Room Required
15:30 to 16:00	Soren Riis Queen Mary University of London Sporadic propositional proofs	Room 1
16:00 to 16:30	Nicola Galesi Resolution by pebbling games	Room 1
18:45 to 19:30	Dinner at Wolfson Court (Residents only)	No Room Required

Wednesday 12th April 2006
09:30 to 10:30	Toniann Pitassi University of Toronto Using lower bounds in proof complexity	Room 1
10:30 to 11:00	Jakob Nordstrom Narrow proofs may be spacious: separating space and width in resolution	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:30	Nathan Segerlind University of Toronto Connections between zero-one programming, communication complexity and proof complexity	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
19:30 to 18:00	Conference Dinner at Christ's College (Dining Hall)	No Room Required

Thursday 13th April 2006
09:30 to 10:30	Iddo Tzameret Tel Aviv University The strength of multilinear proofs	Room 1
10:00 to 10:30	A complete resolution-like calculus for Maxsat	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:30	Parametrised proof complexity	Room 1
12:30 to 13:30	Lunch at Wolson Court	No Room Required
14:00 to 14:30	Pavel Naumov Meta complexity of propositional proofs	Room 1
14:30 to 15:30	Mikhail Alekhnovich University of California On the power of Lovasz-Schrijver hierarchy	Room 1
15:30 to 16:00	Tea	No Room Required
18:45 to 19:30	Dinner at Wolfson Court (Residents only)	No Room Required

Speakers

Mikhail Alekhnovich University of California
Stephen Cook University of Toronto
Nicola Galesi
Russell Impagliazzo University of California
Emil Jerabek University of Toronto
Pavel Naumov
Jakob Nordstrom
Steven Perron University of Toronto
Toniann Pitassi University of Toronto
Chris Pollett
Pavel Pudlak
Soren Riis Queen Mary University of London
Nathan Segerlind University of Toronto
Michael Soltys McMaster University
Neil Thapen Charles University, Prague
Iddo Tzameret Tel Aviv University
Moshe Vardi Rice University

Show All

Workshop theme

Applications for this workshop are now closed

Timetable

Speakers

Supported By

Register for updates