09:00 to 09:25 Registration 09:25 to 09:30 Welcome from John Toland (INI Director) & Annoucements INI 1 09:30 to 10:30 Complexity of computations and proofs and pseudo-finite structures Problems to establish lower bounds for circuit size or for lengths of propositional proofs can be formulated as problems to construct expansions of pseudo-finite structures. I will explain this relation, give a few examples, and discuss some recent work aimed at proof complexity. INI 1 10:30 to 11:00 Morning Coffee 11:00 to 11:30 N Galesi (Università degli Studi di Roma La Sapienza)Proof Complexity of Paris-Harrington Tautologies We study the proof complexity of Paris-Harrington’s Large Ramsey Theorem for bicolorings of graphs. We prove a conditional lower bound in Resolution and a upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in Res(2). We show that under such assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by adapting some constructions due to Erdo ̋s and Mills. INI 1 11:30 to 12:30 S Kreutzer (Technische Universität Berlin)Logical Methods in the Complexity Analysis of Graph Algorithms A classical observation in complexity theory is that many common algorithmic problems on graphs are hard to solve. Consequently, much work has gone into studying restricted classes of admissible inputs on which tractability results can be retained. A particular rich source of structural properties which guarantee the existence of efficient algorithms for many problems on graphs come from structural graph theory, especially algorithmic graph minor theory. It has been found that most generally hard problems become tractable on graph classes of bounded tree-width and many remain tractable on planar graphs or graph classes excluding a fixed minor. Besides many specific results giving algorithms for individual problems, of particular interest are results that establish tractability of a large class of problems on specific classes of instances. These results come in various flavours. In this tutorial we will focus on results that take a descriptive approach, i.e. results that use a logic to describe algorithmic problems and then establish general tractability results for all problems definable in that logic on specific classes of inputs. These results are usually referred to as algorithmic meta-theorems. In some sense the first theorem of this form is Courcelle's famous result that all monadic second-order definable problems are solvable in linear time on all classes of structures of bounded tree-width. Subsequently many further theorems of this form and many tools for obtaining such results have been developed. In this tutorial we will present the main methods and results obtained in this area. In the first part, the focus will be on logical tools that can be used to obtain algorithmic meta-theorems. In the second part of the tutorial we will focus on methods to establish corresponding lower bounds, i.e. intractability results for particular logics on classes of graphs that do not have any of the nice properties that make algorithmic meta-theorems possible. In particular, we will present a reasonably tight lower bound for Courcelle's theorem mentioned above. INI 1 12:30 to 13:30 Lunch at Wolfson Court 14:00 to 15:00 S Dantchev (Durham University)Parameterised Proof Complexity I will start by introducing the basic notion of a parameterised proof as defined by B. Martin, S. Szeider and myself back in 2007, and will discuss a complexity gap theorem theorem for generic parameterisation of tree-like resolution. I will then move onto results that have been obtained since them by various researchers, including parameterised lower bounds for the pigeon-hole principle in resolution and for the maximum clique in random graphs in tree-like resolution. I will conclude with some new results due to B. Martin and myself on parameterised proofs for W[1] as well as with some open problems. INI 1 15:00 to 15:30 Parameterized Complexity of DPLL Search Procedures We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game which models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k-clique requires $n^{\Omega(k)}$ steps for a non-trivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked in [BGLR11] of understanding the Resolution complexity of this family of formulas. INI 1 15:30 to 16:00 Afternoon Tea 16:00 to 16:30 Model Checking for Modal Intuitionistic Dependence Logic In this paper we consider the complexity of model checking for modal intuitionistic dependence logic (MIDL). MIDL is a natural variant of first-order dependence logic (D), which was introduced by Väänänen (2007), as a new approach to independence-friendly logic (Hintikka, Sandu, 1989). Sentences of D have exactly the same expressive power as sentences of existential second-order logic (Väänänen 2007, c.f. Enderton, 1970 and Walkoe, 1970). The compositional semantics of D is team semantics, originally developed by Hodges (1997) for independence-friendly logic. Abramsky and Väänänen (2009) studied Hodges’ construction in a more general context and introduced BID-logic, which extends dependence and includes intuitionistic implication, Boolean disjunction, as well as linear implication. It was shown that the intuitionistic fragment of BID-logic, called intuitionistic dependence logic, has exactly the same expressive power as the full second-order logic, on the level of sentences (Yang, 2010). The modal version of D, modal dependence logic (MDL) was defined by Väänänen (2008). A natural variant of MDL is modal intuitionistic dependence logic, where the intuitionistic implication and Boolean disjunction are added into the setting. In this paper we show that the model checking problem for MIDL in general is PSPACE-complete. Furthermore, we consider fragments of MIDL built by restricting the operators allowed in the logic. It turns out that apart from known NP-complete as well as tractable fragments there also are some coNP-complete fragments, e.g. propositional intuitionistic dependence logic. INI 1 16:30 to 17:30 Complexity results for dependence logic Dependence Logic, introduced by Jouko Väänänen in 2007, is a new logic incorporating the concept of dependence into first-order logic. The expressive power of dependence logic coincides with that of existential second-order logic, and the complexity class NP over finite structures. In the past few years, dependence logic has grown into a new framework in which various notions of dependence and independence can be formalized. We review recent results regarding the expressive power and complexity of certain fragments and extensions of dependence logic. INI 1 17:30 to 18:00 Drinks Reception
 09:00 to 10:00 Y Chen (Shanghai Jiao Tong University)From almost optimal algorithms to logics for complexity classes via listings and a halting problem Let $C$ denote one of the complexity classes polynomial time,'' logspace,'' or nondeterministic logspace.'' We introduce a logic $L(C)_{\mathrm{inv}}$ and show generalizations and variants of the equivalence ($L(C)_{\mathrm{inv}}$ captures $C$ if and only if there is an almost $C$-optimal algorithm in $C$ for the set TAUT of tautologies of propositional logic.) These statements are also equivalent to the existence of a listing of subsets in $C$ of TAUT by corresponding Turing machines and equivalent to the fact that a certain parameterized halting problem is in the parameterized complexity class $\mathrm{XC}_{\rm uni}$. INI 1 10:00 to 10:30 M Lauria (Academy of Sciences of the Czech Republic)Space Complexity of Polynomial Calculus (joint work with Yuval Filmus, Jakob Nordstrom, Neil Thapen, Noga Zewi) During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving, and so research has mostly focused on weak systems that are used by SAT solvers. There has been a relatively long sequence of papers on space in resolution and resolution-based proof systems, and it is probably fair to say that resolution is reasonably well understood from this point of view. For other natural candidates to study, however, such as polynomial calculus or cutting planes, very little has been known. We are not aware of any nontrivial space lower bounds for cutting planes, and for polynomial calculus the only lower bound has been for CNF formulas of unbounded width in [Alekhnovich et al.'02], where the space lower bound is smaller than the initial width of the clauses in the formulas. Thus, in particular, it has been consistent with current knowledge that polynomial calculus could be able to refute any k-CNF formula in constant space. In this paper, we prove several new results on space in polynomial calculus (PC), and in the extended proof system polynomial calculus resolution (PCR) studied in [Alekhnovich et al.'02]: 1. We prove an Omega(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHP^m_n with m pigeons and n holes, and show that this is tight. 2. For PCR, we prove an Omega(n) space lower bound for a bitwise encoding of the functional pigeonhole principle with m pigeons and n holes. These formulas have width O(log(n)), and so this is an exponential improvement over [Alekhnovich et al.'02] measured in the width of the formulas. 3. We then present another encoding of a version of the pigeonhole principle that has constant width, and prove an Omega(n) space lower bound in PCR for these formulas as well. 4. Finally, we prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not obviously the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into a 3-CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other well-studied formula families in proof complexity. INI 1 10:30 to 11:00 Mornign Coffee 11:00 to 11:30 Toda's theorem in bounded arithmetic with parity quantifiers and bounded depth proof systems with parity gates The "first part" of Toda's theorem states that every language in the polynomial hierarchy is probabilistically reducible to a language in $\oplus P$. The result also holds for the closure of the polynomial hierarchy under a parity quantifier. We use Jerabek's framework for approximate counting to show that this part of Toda's theorem is provable in a relatively weak fragment of bounded arithmetic with a parity quantifier. We discuss the significance of the relativized version of this result for bounded depth propositional proof systems with parity gates. Joint work with Sam Buss and Konrad Zdanowski. INI 1 11:30 to 12:30 NP search problems: Provability and reducibilities This is the second of two tutorial talks on total NP search problems. Full abstract not yet available. INI 1 12:30 to 13:30 Lunch at Wolfson Court 14:00 to 15:00 Descriptive complexity of linear algebra An important question that has motivated much work in finite model theory is that of finding a logical characterisation of polynomial-time computability. That is to say, to find a logic in which a class of finite structures is expressible if, and only if, membership in the class is decidable in deterministic polynomial time (PTIME). Much of the research in this area has focused on the extension of inflationary fixed-point logic by counting terms (FPC). This logic has been shown to capture polynomial time on many natural classes of structures, including all classes of graphs with excluded minors. At the same time, it is also known that FPC is not expressive enough to capture polynomial time on the class of all finite graphs. Noting that the various examples of properties in PTIME that are not definable in FPC can be reduced to testing the solvability of systems of linear equations, Dawar et al. (2009) introduced the extension of fixed-point logic with operators for expressing matrix rank over finite fields (FPR). Fixed-point rank logic strictly extends the expressive power of FPC while still being contained in PTIME and it remains an open question whether there are polynomial-time properties that are not definable in this logic. In this talk I give an overview of the main results in the logical study of linear algebra and present new developments in this area. After reviewing the background to this study, I define logics with rank operators and discuss some of the properties that can be expressed with such logics. In order to delimit the expressive power of FPR, I present variations of Ehrenfeucht-Fraïssé games that are suitable for proving non-definability in finite-variable rank logics. Using the rank games, I show that if we restrict to rank operators of arity two, then there are graph properties that can be defined by first-order logic with rank over GF(p) that are not expressible by any sentence of fixed-point logic with rank over GF(q), for all distinct primes p and q. Finally, I discuss how we can suitably restrict these rank games to get an algebraic game equivalence that can be decided in polynomial time on all classes of finite structures. As an application, this gives a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the well-known Weisfeiler-Lehman method. INI 1 15:00 to 15:30 Definability of linear equation systems over groups and rings (joint work with A. Dawar, E. Grädel, B. Holm, E. Kopczynski) One of the major open question in finite model theory is whether there is a logic for PTIME. As one promising candidate, fixed-point logic with counting, FPC, has been studied extensively, and indeed, FPC has been shown to capture PTIME on important classes of structures. Although Cai, Fürer and Immerman ruled out FPC for the general case already in 1992, it was only in 2007 that Atserias et. al [1] found a class of natural problems explaining the major shortcoming of FPC. Specifically, they proved that the important problem of solving linear equation systems (SLES) over finite Abelian groups cannot be expressed in FPC; moreover, all other known queries separating FPC from PTIME turned out to be reducible to SLES via simple logical reductions. Hence, problems from algebra provide a new source of operators which have polynomial-time data complexity and which might be used to strictly extend the expressive power of FPC (cf. the notion of rank logics [2]). Motivated by these insights, we study SLES over various classes of finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in FPC. Based on the structure theory of finite rings, we prove that on important classes of rings, SLES can be reduced to SLES over cyclic groups, which constitute the most basic class of tractable domains for SLES. Furthermore, we prove closure properties for classes of queries that reduce to SLES over fixed rings. As one application, these closure properties provide normal forms for logics extended with solvability operators. [1] Albert Atserias, Andrei A. Bulatov, and Anuj Dawar. Affine systems of equations and counting infinitary logic. Theor. Comput. Sci., 2009. [2] Anuj Dawar, Martin Grohe, Bjarki Holm, and Bastian Laubner. Logics with rank operators. In LICS ’09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science, 2009 INI 1 15:30 to 16:00 Afternoon Tea 16:00 to 16:30 Proof complexity of circuit lower bounds Techniques that could resolve P vs. NP are considerably restricted by well-known barriers in computational complexity. There are several corresponding results in logic stating that certain fragments of arithmetic are not sufficiently strong to prove that P differs from NP or some similar conjectures. We investigate possible extensions of these barriers to stronger theories. Mainly, Razborov's conjecture about hardness of Nisan-Wigderson generators for Extended Frege systems and natural proofs in proof systems admitting feasible disjunction property pointed out by Rudich. INI 1 16:30 to 17:30 Developing logical theories for several NP search classes We present finitely-axiomatizable two-sorted first-order theories associated with several NP search classes in the sense that search problems in a class are precisely those that are provable total in the associated theory. These theories are in the same vein as the family of theories associated with many subclasses of polytime, developed earlier by Nguyen and Cook. We consider proving several theorems in these new theories. (Joint work with Antonina Kolokolova.) INI 1
 09:00 to 10:00 Fragments of approximate counting We pose the question: are there any simple sentences, provable using bounded induction, that cannot already be proved using approximate counting of simple sets? More precisely, we study the long-standing open problem of giving $\forall \Sigma^b_1$ separations for fragments of bounded arithmetic in the relativized setting, but rather than considering the usual fragments defined by the amount of induction they allow, we study Jerabek's theories for approximate counting and their subtheories. We prove separations for some of the subtheories, and also give new propositional translations, in terms of random resolution refutations, for the consequences of $T^1_2$ augmented with a certain weak pigeonhole principle. Joint work with Sam Buss and Leszek Kolodziejczyk. INI 1 10:00 to 10:30 Root finding in TC^0 and open induction It is known that elementary arithmetic operations are computable in uniform TC^0, and some (multiplication, division) are even complete for this complexity class. The corresponding theory of bounded arithmetic, VTC^0, duly defines addition, multiplication, and ordering, and proves that integers form a discretely ordered ring under these operations. It is a natural question what other first-order properties of elementary arithmetic operations are provable in VTC^0. In particular, we are interested whether VTC^0 (or a theory of similar strength) can prove open induction in the basic language of arithmetic (Shepherdson's theory IOpen). This turns out equivalent to the problem whether there are TC^0 root-finding algorithms for constant-degree polynomials whose soundness is provable in VTC^0. In this talk, we will establish that such root-finding algorithms exist in the real (or rather, complex) world, and we will discuss the prospects of their formalization in bounded arithmetic. INI 1 10:30 to 11:00 Morning Coffee 11:00 to 11:30 Infinitary methods in finite model theory The accepted wisdom is that standard techniques from classical model theory fail to apply in the finite. We attempt to dispel this notion by presenting new proofs of the Gaifman and Hanf locality theorems, as they appear in Libkin's textbook on finite model theory. In particular, using compactness over an expanded vocabulary, we obtain strikingly simple arguments that apply over both finite and infinite structures -- all without the complexity of Ehrenfeucht–Fraïssé games normally used. Our techniques rely on internalizing most of the relevant mathematical features into the first-order theory itself. It remains to be seen whether these methods can be extended to proving order-invariant locality. INI 1 11:30 to 12:30 Locality from circuit lower bounds We study the locality of an extension of first-order logic that captures graph queries computable in AC0, i.e., by families of polynomial-size constant-depth circuits. The extension considers first-order formulas over finite relational structures which may use arbitrary numerical predicates in such a way that their truth value is independent of the particular interpretation of the numerical predicates. We refer to such formulas as Arb-invariant FO. In this talk I will show how to use circuit lower bounds for proving that Arb-invariant FO queries are Gaifman-local in the following sense: They cannot distinguish between two tuples that have the same neighborhood up to distance (log n)^c, where n represents the number of elements in the structure and c is a constant depending on the query. INI 1 12:30 to 13:30 Lunch at Wolfson Court