View: session overviewtalk overviewside by side with other conferences
10:45  Opening SPEAKER: Olaf Beyersdorff 
11:00  On Some Conjectures in Proof Complexity SPEAKER: Pavel Pudlák ABSTRACT. Our aim is to study conjectures that are somehow connected with consistency and/or incompleteness of first order theories. We want to fully understand (1) how far we can go by considering stronger and stronger conjectures and (2) whether the system of conjectures splits into incomparable ones or there there are always stronger unifying conjectures. Currently the conjectures that we have can be classified into two levels  uniform and nonunifom, and two directions  universal and existential. We still hope to be able to find a stronger unifying conjecture. 
12:00  SizeSpace Bounds and Tradeoffs for CDCL Proofs SPEAKER: Marc Vinyals ABSTRACT. A long line of research has shown that conflictdriven clause learning viewed as a proof system can polynomially simulate resolution. We give a more explicit description of this CDCL proof system, which allows us to define proof size and space in a natural way and also capture aspects such as clause learning schemes and restart policies. This in turn makes it possible to study which upper and lower bounds on size, space and sizespace tradeoffs in general resolution carry over to proofs actually realizable by CDCL solvers. 
12:30  Beyond QResolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction SPEAKER: Hubie Chen ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a firstorder sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Qresolution proof system in a broader context, and also allows us to derive QCSP tractability results. 
14:30  A (Biased) Survey of Space Complexity and TimeSpace Tradeoffs in Proof Complexity SPEAKER: Jakob Nordström ABSTRACT. This presentation is intended as a survey of results on proof space and timespace tradeoffs in proof complexity. We will try to provide some proof sketches to give a flavour of the proof methods used, but also explain the limitations of current techniques and state some tantalising problems that remain open. 
15:30  Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds SPEAKER: Marc Vinyals ABSTRACT. Recently, an active line of research has been into the space complexity of proofs. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PC space. This yields formulas that exhibiting a degreespace separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4regular graphs almost surely require space at least Ω(√n). Our proofs use techniques from [BonacinaGalesi '13]. Our final contribution, however, is to show that these techniques cannot yield nonconstant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space. 
16:30  Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomialtime SPEAKER: JeanJose Razafindrakoto ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial Given a class S of provably total NP search problems for some theory, the general aim of our research project is to identify some specific provably total NP search problem class (usually defined via some specific combinatorial principle) which is complete within S under AC^{0}manyone reduction; completeness should be proven using AC^{0}reasoning only, i.e. formalizable in V_{0}. For example, it was shown by Cook and Nguyen that PLS, where the neighborhood function and the initial point are given by AC^{0}functions, is complete in the above sense for the class of provably total NP search problems in T^{1}_{2}. For the theory related to polynomialtime, we identify the search problem class Inflationary Iteration (IITER) which serves our above described aim. A function F (defined on finite strings) is inflationary if X is a subset of F(X) (under the natural identification of strings with finite sets). An IITER principle is defined as a special case of the iteration principle, in which the iterated function has to be AC^{0}computable and inflationary. Cook and Nguyen have a generic way of defining a bounded arithmetic theory V_{C} for complexity classes C below polynomialtime. For such theory V_{C}, we define a search problem class KPT[C] which serves our above described aim. These problems are based on a version of Herbrand's theorem proven by Krajicek, Pudlak and Takeuti. 
17:00  Parameterfree induction in bounded arithmetic SPEAKER: Emil Jeřábek ABSTRACT. In the area of strong fragments of Peano Arithmetic, it proved fruitful to study not just the usual induction fragments IΣ_{i}, but also fragments axiomatized by parameterfree induction schemata, and theories axiomatized using the closely related induction inference rules. In contrast, induction rules and parameterfree schemata have been largely ignored in bounded arithmetic literature. Apart from IE_{i }briefly discussed by Kaye (1990), the corresponding fragments of Buss's S_{2} were only studied by Bloch (1992) and CordonFranco et al. (2009). Many basic questions about these fragments were disregarded, in particular, neither paper even mentions Π^{b}_{i}induction rules and parameterfree schemata, despite that they could be expected to behave rather differently from Σ^{b}_{i}rules by analogy with the case of strong fragments. In this talk, we will try to systematically investigate parameterfree and inference rule versions of the theories T^{i}_{2} and S^{i}_{2}. We will particularly focus on the following questions:

17:30  Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic SPEAKER: Ján Pich ABSTRACT. The aim of this presentation is to show that a lot of complexity theory can be formalized in low fragments of arithmetic like Cook's theory PV_{1. }We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV_{1 }(no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n,d,λ)graphs needed to derive the PCP theorem in PV_{1}. 