08:30 to 10:00 Registration 10:00 to 11:00 P Pudlak ([Academy of Sciences, Prague])$On \forall\Sigma_1^b$ sentences provable in bounded arithmetic We shall give a characterization of \forall\Sigma_1^b sentences provable in theories S_2^i. We shall consider also certain unrestricted versions of the principles that characterize these sentences and prove that they require iterated exponential time. This gives partial evidence that the hierarchy of \forall\Sigma_1^b sentences provable in S_2^i is strictly increasing. INI 1 , 11:00 to 11:30 Coffee 11:30 to 12:00 P Nguyen ([Toronto])The complexity of proving the discrete Jordan Curve theorem and related principles The Jordan Curve Theorem states that a simple, closed curve divides the plane into exactly two connected components. We consider the discrete'' version of this theorem (JCT) where the curve lies in an nxn grid. The Theorem can be formalized as either true statements in Bounded Arithmetic or families of propositional tautologies. Here we show that the formalizations in Bounded Arithmetic are provable in some weak theories (i.e., V^0 and V^0(2)); this implies that the families of tautologies have short proofs in the corresponding propositional proof systems. First, we formalize the theorem when the simple curve is given as a sequence of edges on the grid. We show that in this case the theorem can be proved in the theory V^0. Next, we consider the case where the input is a set of edges which generally form multiple simple closed curves. The interesting conclusion here is that the set of edges divides the plane into at least two connected components. We show that this is indeed provable in the theory V^0(2). The related principles include the STCONN on grid graph considered by Buss [Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies] and the nonplanarity of K3,3. STCONN is reducible to JCT, and thus it is provable in V^0(2). This improves Buss's result (that STCONN has polysize proof in TC^0-Frege). INI 1 , 12:00 to 12:30 A Beckmann ([Wales])Uniform proof complexity One main aim in Propositional Proof Complexity is to prove strong lower bounds for a general propositional proof system. Inspired by this program, we will introduce uniform reducts of propositional proof systems. Uniform reducts are sets of first order formulas of arithmetic which are defined using translations from first order formulas to propositional formulas. We will describe basic properties of uniform reducts, discuss their relationship to Cook's Programme, and explain some more advanced features of them. Recently, Steve Cook made an obervation relating the study of uniform reducts to the existence of optimal proof systems - if time permits we will touch on this as well. INI 1 , 12:30 to 13:30 Lunch at Wolfson Court 14:00 to 15:00 N Thapen ([Academy of Sciences, Prague])$T^1_2, T^2_2$ and search problems We give some new, natural principles characterizing the \Sigma^b_1 consequences of these theories, based on a reflection principle for resolution. INI 1 15:00 to 15:30 Tea 15:30 to 16:00 E Jerabek ([Toronto])Approximate counting in bounded arithmetic We use the dual weak pigeonhole principle to develop approximate counting in bounded arithmetic. As an application, we show how to formalize classes of randomized algorithms, such as BPP. INI 1 , 16:00 to 16:30 C Pollett (San José State University)When can $S^1_2$ prove the weak pigeonhole principle? It is well known result of Krajicek and Pudlak that if $S^1_2$ could prove the injective weak pigeonhole principle for every polynomial time function then RSA would not be secure. In this talk, we will consider function algebras based on a common characterization of the polynomial time functions where we slightly modify the initial functions and further restrict the amount of allowable recursion. We will then argue that $S^1_2$ can prove the surjective weak pigeonhole principle for functions in this algebra. INI 1 , 17:00 to 18:00 Wine and Beer Reception 18:45 to 19:30 Dinner at Wolfson Court (Residents only)
 09:30 to 10:30 S Cook ([Toronto])Capturing complexity classes by their reasoning power For each of many standard complexity classes within NP we associate a canonical set of universal and existential theorems which are those which can be proved using concepts in the class. In some cases we can also associate canonical proof systems in the quantified propositional calculus. INI 1 , 10:30 to 11:00 M Vardi ([Rice])Constraint propagation as a proof system Refutation proofs can be viewed as a special case of constraint propagation, which is a fundamental technique in solving constraint-satisfaction problems. The generalization lifts, in a uniform way, the concept of refutation from Boolean satisfiability problems to general constraint-satisfaction problems. On the one hand, this enables us to study and characterize basic concepts, such as refutation width, using tools from finite-model theory. On the other hand, this enables us to introduce new proof systems, based on representation classes, that have not been considered up to this point. We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations, and compare their strength to well-known proof systems, such as resolution, the Gaussian calculus, cutting planes, and Frege systems of bounded alternation-depth. In particular, we show that refutations by ODBBs polynomially simulate resolution and can be exponentially stronger. Joint work with Albert Atserias and Phokion Kolaitis. INI 1 , 11:00 to 11:30 Coffee 11:30 to 12:00 M Soltys ([McMaster])The proof complexity of matrix algebra There are fast parallel algorithms for computing the characteristic polynomial of a matrix: notably Berkowitz's and Csanky's algorithms. While these algorithms run in NC2, all the known proofs of correctness require polynomial time concepts. Are there quasi-polynomial Frege (i.e., NC2-Frege) proofs of correctness of these algorithms? Or is it the case the universal matrix identities separate Frege and Extended Frege? This talk will address these questions and present recent progress in this area. INI 1 12:00 to 12:30 S Perron ([Toronto])A minimal quantified proof system for polytime reasoning INI 1 12:30 to 13:30 Lunch at Wolfson Court 14:00 to 15:00 R Impagliazzo ([California, San Diego])Which SAT instances are the hardest? INI 1 15:00 to 15:30 Tea 15:30 to 16:00 S Riis ([London])Sporadic propositional proofs The following feature is shared by certain weak propositional proof systems: If $\psi_n$ is a uniformly generated sequence of propositional formula, and the sequence $\psi_n$ has polynomial size proofs, then the sequence $\psi_n$ in fact has polynomial size proofs that are generated in an uniform manner . For stronger propositional proof systems (like the Frege Proof Systems) this feature might fail and sporadic proofs (that are not instances of a sequence of uniform proofs) might exist. In the talk I will argue that understanding and limiting the behaviour of these sporadic proofs could be crucial for any serious progress in Propositional Proof Complexity. INI 1 , 16:00 to 16:30 N Galesi ([Rome])Resolution by pebbling games We present an approach to study the complexity of refutations in Resolution by means of certain pebbling games. We will define certain classes of such games that allow to obtain a new frame for: (1) proving size lower bounds in Resolution; (2) devising new algorithms to find Resolution refutations; (3) characterizing the hardness of provability in Resolution as an "almost" satisfiability. We'll discuss about how to extend a similar approach to stronger systems than Resolution. INI 1 18:45 to 19:30 Dinner at Wolfson Court (Residents only)
 09:30 to 10:30 I Tzameret ([Tel Aviv])The strength of multilinear proofs We discuss an algebraic proof system that manipulates multilinear arithmetic formulas. We show this proof system to be fairly strong even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, algebraic proofs manipulating depth 3 multilinear arithmetic formulas are strictly stronger than Resolution, Polynomial Calculus (and Polynomial Calculus with Resolution); and (over characteristic 0) admit polynomial-size proofs of the (functional) pigeonhole principle. Finally, we illustrate a connection between lower bounds on multilinear proofs and lower bounds on multilinear arithmetic circuits. INI 1 , 10:00 to 10:30 ML Bonet ([Barcelona])A complete resolution-like calculus for Maxsat Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound. Joint work with Jordi Levy and Felip Manya. INI 1 11:00 to 11:30 Coffee 11:30 to 12:30 S Dantchev ([Durham])Parametrised proof complexity Motivated by the well known concept of Fixed-Parameter Tractability, we initiate research in an area that we call Parametrised Proof Complexity. We first give a Cook-Rekhow-style definition of a parametrised proof system, and then relate the (im)possibility of existence of a fixed-parameter tractable (FPT) proof system to the FPT vs W[2] question. We observe that the most popular method for designing fixed-parameter algorithms, Bounded Search Tree, corresponds to Tree-like Resolution in the context of parametrised proof systems, and give some upper and lower bounds for the latter. We finally discuss and prove some dichotomy results (also called complexity gap theorems) for weak relativised proof systems. This is a work in progress, joint with B. Martin and S. Szeider. INI 1 , 12:30 to 13:30 Lunch at Wolson Court 14:00 to 14:30 P Naumov (McDaniel College)Meta complexity of propositional proofs INI 1 14:30 to 15:30 M Alekhnovich ([California, San Diego])On the power of Lovasz-Schrijver hierarchy Lov\'{a}sz and Schrijver described a generic method of tightening the LP and SDP relaxation for any $0$-$1$ optimization problem. These tightened relaxations were the basis of several celebrated approximation algorithms (such as for MAX-CUT, MAX-3SAT, and SPARSEST CUT). In this talk I will survey recent lower bounds for the number of rounds in this model for well-known problems such as MAX-SAT, Hypergraph Vertex Cover and Minimum Set Cover. Also I will elaborate why these lower bounds are encoding dependent, in particular the standard NP reductions do not seem to work in this model. This fact leads to the wide list of open problems, which appear important for proof complexity, computational complexity and algorithm design. INI 1 15:30 to 16:00 Tea 18:45 to 19:30 Dinner at Wolfson Court (Residents only)