Logical Approaches to Barriers in Complexity II
Monday 26th March 2012 to Friday 30th March 2012
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 pseudofinite structures
Problems to establish lower bounds for circuit size or for lengths of propositional proofs can be formulated as problems to construct expansions of pseudofinite 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 ParisHarrington Tautologies
We study the proof complexity of ParisHarrington’s Large Ramsey Theorem for bicolorings of graphs. We prove a conditional lower bound in Resolution and a upper bound in boundeddepth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasipolynomial) Pigeonhole principle in Res(2). We show that under such assumption, there is no refutation of the ParisHarrington formulas of size quasipolynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blowup 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 treewidth 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 metatheorems.
In some sense the first theorem of this form is Courcelle's famous result that all monadic secondorder definable problems are solvable in linear time on all classes of structures of bounded treewidth. 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 metatheorems.
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 metatheorems 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 treelike resolution. I will then move onto results that have been obtained since them by various researchers, including parameterised lower bounds for the pigeonhole principle in resolution and for the maximum clique in random graphs in treelike 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 ProverDelayer game which models the running time of DPLL procedures and we establish an informationtheoretic 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 kclique requires $n^{\Omega(k)}$ steps for a nontrivial distribution of graphs close to the critical threshold. For the restricted case of treelike 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 firstorder dependence logic (D), which was introduced by Väänänen (2007), as a new approach to independencefriendly logic (Hintikka, Sandu, 1989). Sentences of D have exactly the same expressive power as sentences of existential secondorder 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 independencefriendly logic. Abramsky and Väänänen (2009) studied Hodges’ construction in a more general context and introduced BIDlogic, which extends dependence and includes intuitionistic implication, Boolean disjunction, as well as linear implication. It was shown that the intuitionistic fragment of BIDlogic, called intuitionistic dependence logic, has exactly the same expressive power as the full secondorder 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 PSPACEcomplete. Furthermore, we consider fragments of MIDL built by restricting the operators allowed in the logic. It turns out that apart from known NPcomplete as well as tractable fragments there also are some coNPcomplete 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 firstorder logic. The expressive power of dependence logic coincides with that of existential secondorder 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 
A Atserias (Universitat Politècnica de Catalunya) Indistinguishability in Counting Logics and the Complexity of SemiAlgebraic Proofs
The recent connection between the concept of indistinguishability by the properties expressible in a certain formal language and a relaxation of structural isomorphism through linear programming brings the areas of descriptive complexity and propositional proof complexity a little bit closer together. In this talk I will overview this connection making emphasis on the questions it has answered, but also on the many new exciting questions that it raises.

INI 1  
10:00 to 10:30 
The hierarchy of equivalence relations on the natural numbers under computable reducibility
Many of the naturally arising equivalence relations in mathematics, such as isomorphism relations on various types of countable structures, turn out to be equivalence relations on a standard Borel space, and these relations form an intensely studied hierarchy under Borel reducibility. The topic of this talk is to introduce and explore the computable analogue of this robust theory, by studying the corresponding hierarchy of equivalence relations on the natural numbers under computable reducibility. Specifically, one relation E is computably reducible to another, F , if there is a unary computable function f such that x E y if and only if f(x) F f(y) . This gives rise to a very different hierarchy than the Turing degrees on such relations, since it is connected with the difficulty of the corresponding classification problems, rather than with the difficulty of computing the relations themselves. The theory is well suited for an analysis of equivalence relations on classes of c.e. structures, a rich context with many natural examples, such as the isomorphism relation on c.e. graphs or on computably presented groups. An abundance of open questions remain, and the subject is an attractive mix of methods from mathematical logic, computability, set theory, particularly descriptive set theory, and the rest of mathematics, subjects in which many of the equivalence relations arise. This is joint work with Sam Coskey and Russell Miller.

INI 1  
10:30 to 11:00  Morning Coffee  
11:00 to 11:30 
Ordinal Strength of LogicEnriched Type Theories
Type theories are formal languages that can be read as either a programming language or a system of logic, via the propositionsastypes or proofsasprograms paradigm. Their syntax and metatheory is quite different in character to that of "orthodox logics" (the familiar firstorder logics, secondorder logics, etc). So far, it has been difficult to relate type theories to the more orthodox systems of firstorder logic, secondorder logic, etc.
Logicenriched type theories (LTTs) may help with this problem. An LTT is a hybrid system consisting of a type theory (for defining mathematical objects) and a separate logical component (for reasoning about those objects). It is often possible to translate between a type theory and an orthodox logic using an LTT as an intermediate system, when finding a direct translation would be very difficult.
In this talk, I shall summarise the work so far on the proof theory of type theories, including Anton Setzer's work on ordinal strength. I shall show how LTTs allow results about type theories to be applied to orthodox logics, and vice versa. This will include a recently discovered, elementary proof of the conservativity of ACA0 over PA. I conclude by giving two new results: typetheoretic analogues of the classic results that P corresponds to firstorder least fixed point logic, and NP to secondorder existential logic.

INI 1  
11:30 to 12:30 
S Kreutzer (Technische Universität Berlin) Logical Methods in the Complexity Analysis of Graph Algorithms II
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 treewidth 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 metatheorems.
In some sense the first theorem of this form is Courcelle's famous result that all monadic secondorder definable problems are solvable in linear time on all classes of structures of bounded treewidth. 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 metatheorems.
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 metatheorems 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 
The complexity of enumeration and counting for acyclic conjunctive queries
Enumerating all the solutions of a problem or counting the number of these solutions are two related algorithmic tasks. Complexity measures, however, are of a different nature. For enumeration problem, for example, one of the main notion is that of delay between generated solutions. A problem is considered as tractable if one can enumerate the solutions one by one without repetition with a "reasonable" delay (e.g. polynomial, linear or constant time) between two solutions.
In this talk, we will make a tour on the complexity of enumeration and
(weighted) counting for acyclic conjunctive queries (ACQ), a wellknown tractable fragment (for decision) of conjunctive queries.
We first show that there is a dichotomy for enumeration and, up to some reasonable complexity assumption, such queries are either enumerable with a linear or with a "constant" delay. Hence, in all cases, enumeration is tractable.
For weighted counting, the situation is more complex. The unweighted quantifier free version of this problem is known to be tractable (for combined complexity), but it is also known that introducing even a single quantified variable makes it #Phard. By introducing some polynomial representation of queries, we first show that weighted counting for quantifierfree ACQ is still tractable and that even minimalistic extensions of the problem lead to hard cases. We then introduce a new parameter for quantified queries that permits to isolate large island of tractability. We show that, up to a standard assumption from parameterized complexity, this parameter fully characterizes tractable subclasses for counting weighted solutions of ACQ queries. This completely determine the tractability frontier for weighted counting in this case.

INI 1  
15:00 to 15:30 
Bounded degree and planar spectra
There are many problems in finite model theory about which we know a lot in the unrestricted classes, but which are still not thoroughly researched in the case where we restrict the class of considered models (for example, in terms of properties of their Gaifman graphs). In this talk we consider the problem of spectra of formulae. A set of integers S is a spectrum of phi if n \in S iff phi has a model of size n. It is well known that S is a spectrum of some formula iff the problem of deciding whether n \in S is in NP when n is given in unary (equivalently, in NE when n is given in binary).
Restricting the class of models we can get, for example, bounded degree spectra (S is a bounded degree spectrum of phi iff phi has a bounded degree model of size n), weak planar spectra (S is a bounded degree spectrum of phi iff phi has a planar model of size n), and forced planar spectra (S is a spectrum of phi which admits only planar models).
We provide the complexity theoretic characterizations for these cases, similar to the one above. In case of bounded degree spectra, there is a very small
(polylogarythmic) gap between our lower and upper bound. In case of weak planar spectra the gap is polynomial. We also provide a weaker complexity theoretic characterization of forced planar spectra.

INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 16:30 
SAT Solving: Present and Future
SAT solving experienced exciting developments, especially in the last ten years. It seems fair to say that certain areas of industry, like EDA (Electronic Design Automation) would not be able perform at the current level without "SAT technology".
In the first part of my talk I will give some short overview on this development. Then, in the second part, I want to discuss directions for the future.

INI 1  
16:30 to 17:00  Phase Transitions and Computational Complexity  INI 1  
17:00 to 17:30  Break  
17:30 to 18:30 
A Hodges (University of Oxford) Alan Turing: the creative power of mathematics
Nowadays it is widely acknowledged that Turing's 1936 definition of computability, and his discovery of the concept of the universal machine, provided the foundation for the emergence of the digital computer in 1945. But Turing was not simply a logician. In this talk, I shall bring out how Turing's youthful 1936 work arose from a wide field of enquiry with mathematical, physical and philosophical elements. Then, that Turing's broad approach to mathematics and technology led him through the wartime cryptographic work into his own electronic computer plan of 1945. This extraordinary breadth of knowledge and application also created the setting for his later Artificial Intelligence plans and for his theory of biological growth.

INI 1  
18:30 to 19:00  Drinks Reception 
09:00 to 10:00 
R Santhanam (University of Edinburgh) Strong Lower Bounds for ConstantDepth Frege Imply Lower Bounds for Frege
I will discuss a recent result proved with Yuval Filmus and Toni Pitassi: exponential size lower bounds for constantdepth Frege imply superpolynomial size lower bounds for Frege. The proof is constructive in that it shows how to simulate polynomial size Frege proofs for any sequence of tautologies with subexponential size proofs in constantdepth Frege. The simulation is tight for treelike proofs. I will also mention consequences of the result for weak automatizability of constantdepth Frege.

INI 1  
10:00 to 10:30 
Separations between propositional proof systems related to clause learning
Resolution trees with lemmas (RTL) are a resolutionbased propositional proof system that is related to the DLL algorithm with clause learning, with its fragments RTL(k) being related to clause learning algorithms where the width of learned clauses is bounded by k.
For every k up to O(log n), an exponential separation between the proof systems RTL(k) and RTL(k+1) is shown, indicating that a minimal increase in the width of learned clauses can lead to an exponential speedup for clause learning algorithms.

INI 1  
10:30 to 11:00  Morning Coffee  
11:00 to 11:30 
Towards a New Theory of Bounded Arithmetic for PSPACE computations
I will present a second order extension of wellknown first order theories of bounded arithmetic. The purpose of this work is to find a new prooftheoretic characterisation of the polynomialspace computable functions in terms of bounded arithmetic. This is a joint work with Toshiyasu Arai (Chiba University, Japan) in progress.

INI 1  
11:30 to 12:30 
NP search problems: Complexity and reducibilities
This is the first 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 19:30  Free Afternoon  
19:30 to 22:00  Conference Dinner at Christ's College 
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 timespace tradeoffs 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 resolutionbased 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 kCNF 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 3CNF
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 kCNF 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 3CNF in the canonical way,
something that we believe can be useful when proving PCR space
lower bounds for other wellstudied 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 polynomialtime 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 fixedpoint 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 fixedpoint logic with operators for expressing matrix rank over finite fields (FPR). Fixedpoint rank logic strictly extends the expressive power of FPC while still being contained in PTIME and it remains an open question whether there are polynomialtime 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 EhrenfeuchtFraïssé games that are suitable for proving nondefinability in finitevariable 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 firstorder logic with rank over GF(p) that are not expressible by any sentence of fixedpoint 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 polynomialtime approximations of graph isomorphism that is strictly stronger than the wellknown WeisfeilerLehman 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, fixedpoint 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 polynomialtime 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 wellknown 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 NisanWigderson 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 finitelyaxiomatizable twosorted firstorder 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 longstanding 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 firstorder 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 rootfinding algorithms for constantdegree polynomials whose soundness is provable in VTC^0. In this talk, we will establish that such rootfinding 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 firstorder theory itself. It remains to be seen whether these methods can be extended to proving orderinvariant locality.

INI 1  
11:30 to 12:30 
Locality from circuit lower bounds
We study the locality of an extension of firstorder logic that captures graph queries computable in AC0, i.e., by families of polynomialsize constantdepth circuits. The extension considers firstorder 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 Arbinvariant FO.
In this talk I will show how to use circuit lower bounds for proving that Arbinvariant FO queries are Gaifmanlocal 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 