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.

ABSTRACT. A long line of research has shown that conflict-driven 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 size-space trade-offs in general resolution carry over to proofs actually realizable by CDCL solvers.

ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order 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 Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

ABSTRACT. This presentation is intended as a survey of results on proof space and time-space trade-offs 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.

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 degree-space separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4-regular graphs almost surely require space at least Ω(√n).

Our proofs use techniques from [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques cannot yield non-constant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space.

ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial
hierarchy and below polynomial-time. Recent research has tried to characterize the provably total NP search problems
in such theories, where a total NP search problem is provably total in a theory T if it can be formalized in the language of T, and T can prove that, for each instance, there exists a solution to the search problem. For example, Buss and Krajcek showed that the class of provably total NP search problems in a certain bounded arithmetic theory (denoted T¹₂ or  TV₁) is characterized by PLS. Further characterizations for theories above T¹₂ were later discovered. To the best of our knowledge, no such characterizations are known for the theories below T¹₂ until this work.

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⁰-many-one reduction; completeness should be proven using AC⁰-reasoning only, i.e. formalizable in V₀. For example, it was shown by Cook and Nguyen that PLS, where the neighborhood function and the initial point are given by AC⁰-functions, is complete in the above sense for the class of provably total NP search problems in T¹₂.

For the theory related to polynomial-time, 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⁰-computable and inflationary.

Cook and Nguyen have a generic way of defining a bounded arithmetic theory V_C for complexity classes C below polynomial-time. 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.

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 parameter-free induction schemata, and theories axiomatized using the closely related induction inference rules.

In contrast, induction rules and parameter-free 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₂ were only studied by Bloch (1992) and Cordon-Franco et al. (2009). Many basic questions about these fragments were disregarded, in particular, neither paper even mentions Π^b_i-induction rules and parameter-free 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 parameter-free and inference rule versions of the theories Tⁱ₂ and Sⁱ₂. We will particularly focus on the following questions:

• Reductions between the various rules and schemata.
• Conservativity results between the fragments, and the formula complexity of axioms.
• The number of instances (nesting) of R needed to generate the closure T+R, and finite axiomatizability of fragments.
• Reformulation of axioms and rules in terms of reflection principles for propositional proof systems.
• Conditional or relativized separations between the fragments.

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₁ (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₁.