# Workshop Programme

## for period 26 - 30 March 2012

### Logical Approaches to Barriers in Complexity II

26 - 30 March 2012

Timetable

Monday 26 March | ||||

09:00-09:25 | Registration | |||

09:25-09:30 | Welcome from John Toland (INI Director) & Annoucements | |||

09:30-10:30 | Krajicek, J (Charles University, Prague) |
|||

Complexity of computations and proofs and pseudo-finite structures | Sem 1 | |||

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

10:30-11:00 | Morning Coffee | |||

11:00-11:30 | Galesi, N (Università degli Studi di Roma La Sapienza) |
|||

Proof Complexity of Paris-Harrington Tautologies | Sem 1 | |||

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

11:30-12:30 | Kreutzer, S (Technische Universität Berlin) |
|||

Logical Methods in the Complexity Analysis of Graph Algorithms | Sem 1 | |||

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

12:30-13:30 | Lunch at Wolfson Court | |||

14:00-15:00 | Dantchev, S (Durham University) |
|||

Parameterised Proof Complexity | Sem 1 | |||

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

15:00-15:30 | Beyerdorff, O (Università degli Studi di Roma La Sapienza) |
|||

Parameterized Complexity of DPLL Search Procedures | Sem 1 | |||

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

15:30-16:00 | Afternoon Tea | |||

16:00-16:30 | Yang, F (University of Helsinki) |
|||

Model Checking for Modal Intuitionistic Dependence Logic | Sem 1 | |||

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

16:30-17:30 | Kontinen, J (University of Helsinki) |
|||

Complexity results for dependence logic | Sem 1 | |||

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

17:30-18:00 | Drinks Reception |

Tuesday 27 March | ||||

09:00-10:00 | Atserias, A (Universitat Politècnica de Catalunya) |
|||

Indistinguishability in Counting Logics and the Complexity of Semi-Algebraic Proofs | Sem 1 | |||

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

10:00-10:30 | Hamkins, JD (City University of New York) |
|||

The hierarchy of equivalence relations on the natural numbers under computable reducibility | Sem 1 | |||

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

10:30-11:00 | Morning Coffee | |||

11:00-11:30 | Adams, R (University of London) |
|||

Ordinal Strength of Logic-Enriched Type Theories | Sem 1 | |||

Type theories are formal languages that can be read as either a programming language or a system of logic, via the propositions-as-types or proofs-as-programs paradigm. Their syntax and metatheory is quite different in character to that of "orthodox logics" (the familiar first-order logics, second-order logics, etc). So far, it has been difficult to relate type theories to the more orthodox systems of first-order logic, second-order logic, etc. Logic-enriched 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: type-theoretic analogues of the classic results that P corresponds to first-order least fixed point logic, and NP to second-order existential logic. |
||||

11:30-12:30 | Kreutzer, S (Technische Universität Berlin) |
|||

Logical Methods in the Complexity Analysis of Graph Algorithms II | Sem 1 | |||

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

12:30-13:30 | Lunch at Wolfson Court | |||

14:00-15:00 | Durand, A (Université Denis Diderot) |
|||

The complexity of enumeration and counting for acyclic conjunctive queries | Sem 1 | |||

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 well-known 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 #P-hard. By introducing some polynomial representation of queries, we first show that weighted counting for quantifier-free 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. |
||||

15:00-15:30 | Kopczynski, E (Uniwersytet Warszawski) |
|||

Bounded degree and planar spectra | Sem 1 | |||

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

15:30-16:00 | Afternoon Tea | |||

16:00-16:30 | Kullmann, O (Swansea University) |
|||

SAT Solving: Present and Future | Sem 1 | |||

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

16:30-17:00 | Vardi, M (Rice University) |
|||

Phase Transitions and Computational Complexity | Sem 1 | |||

17:00-17:30 | Break | |||

17:30-18:30 | Hodges, A (University of Oxford) |
|||

Alan Turing: the creative power of mathematics | Sem 1 | |||

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

18:30-19:00 | Drinks Reception |

Wednesday 28 March | ||||

09:00-10:00 | Santhanam, R (University of Edinburgh) |
|||

Strong Lower Bounds for Constant-Depth Frege Imply Lower Bounds for Frege | Sem 1 | |||

I will discuss a recent result proved with Yuval Filmus and Toni Pitassi: exponential size lower bounds for constant-depth 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 sub-exponential size proofs in constant-depth Frege. The simulation is tight for tree-like proofs. I will also mention consequences of the result for weak automatizability of constant-depth Frege. |
||||

10:00-10:30 | Johannsen, J (Ludwig-Maximilians-Universität München) |
|||

Separations between propositional proof systems related to clause learning | Sem 1 | |||

Resolution trees with lemmas (RTL) are a resolution-based 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 speed-up for clause learning algorithms. |
||||

10:30-11:00 | Morning Coffee | |||

11:00-11:30 | Eguchi, N (Tohoku University) |
|||

Towards a New Theory of Bounded Arithmetic for PSPACE computations | Sem 1 | |||

I will present a second order extension of well-known first order theories of bounded arithmetic. The purpose of this work is to find a new proof-theoretic characterisation of the polynomial-space computable functions in terms of bounded arithmetic. This is a joint work with Toshiyasu Arai (Chiba University, Japan) in progress. |
||||

11:30-12:30 | Buss, S (University of California, San Diego) |
|||

NP search problems: Complexity and reducibilities | Sem 1 | |||

This is the first of two tutorial talks on total NP search problems. Full abstract not yet available. |
||||

12:30-13:30 | Lunch at Wolfson Court | |||

14:00-19:30 | Free Afternoon | |||

19:30-22:00 | Conference Dinner at Christ's College |

Thursday 29 March | ||||

09:00-10:00 | Chen, Y (Shanghai Jiao Tong University) |
|||

From almost optimal algorithms to logics for complexity classes via listings and a halting problem | Sem 1 | |||

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}$. |
||||

10:00-10:30 | Lauria, M (Academy of Sciences of the Czech Republic) |
|||

Space Complexity of Polynomial Calculus (joint work with Yuval Filmus, Jakob Nordstrom, Neil Thapen, Noga Zewi) | Sem 1 | |||

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

10:30-11:00 | Mornign Coffee | |||

11:00-11:30 | Kolodziejczyk, L (Uniwersytet Warszawski) |
|||

Toda's theorem in bounded arithmetic with parity quantifiers and bounded depth proof systems with parity gates | Sem 1 | |||

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

11:30-12:30 | Buss, S (University of California, San Diego) |
|||

NP search problems: Provability and reducibilities | Sem 1 | |||

This is the second of two tutorial talks on total NP search problems. Full abstract not yet available. |
||||

12:30-13:30 | Lunch at Wolfson Court | |||

14:00-15:00 | Holm, B (University of Cambridge) |
|||

Descriptive complexity of linear algebra | Sem 1 | |||

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

15:00-15:30 | Pakusa, W (RWTH Aachen University) |
|||

Definability of linear equation systems over groups and rings | Sem 1 | |||

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

15:30-16:00 | Afternoon Tea | |||

16:00-16:30 | Pich, J | |||

Proof complexity of circuit lower bounds | Sem 1 | |||

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

16:30-17:30 | Nguyen, PT (Université de Montréal) |
|||

Developing logical theories for several NP search classes | Sem 1 | |||

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.) |

Friday 30 March | ||||

09:00-10:00 | Thapen, N (Academy of Sciences of the Czech Republic) |
|||

Fragments of approximate counting | Sem 1 | |||

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

10:00-10:30 | Jerábek, E (Academy of Sciences of the Czech Republic) |
|||

Root finding in TC^0 and open induction | Sem 1 | |||

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

10:30-11:00 | Morning Coffee | |||

11:00-11:30 | Lindell, S (Haverford College) |
|||

Infinitary methods in finite model theory | Sem 1 | |||

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

11:30-12:30 | Schweikardt, N (Goethe-Universität Frankfurt) |
|||

Locality from circuit lower bounds | Sem 1 | |||

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

12:30-13:30 | Lunch at Wolfson Court |