Logic and Computational Complexity

An International Workshop Series



The Eighteenth International Workshop on Logic and Computational Complexity will be held in Reykjavik, Iceland, on June 19, 2017, as an affiliated meeting of LiCS 2017 .

LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity.

The program will consist of invited lectures as well as contributed papers selected by the Program Committee.


Paper submission deadline: April 14, 2017
Authors' notification: May 1, 2017
Workshop: June 19, 2017


  • Arnaud Durand, Université Denis Diderot - Paris 7
  • Damiano Mazza, CNRS--Université Paris-Nord


09:00-10:00 - Invited talk

Church meets Cook and Levin

Damiano Mazza (CNRS--Université Paris-Nord)

The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory. What would a proof of the Cook-Levin theorem look like if the reference model of computation were not Turing machines but the lambda-calculus? We will see that exploring the alternative universe of "structural complexity with lambda-terms instead of Turing machines" brings up a series of interesting questions, both technical and philosophical. Some of these have satisfactory answers, leading us in particular to a proof of the Cook-Levin theorem using tools of proof-theoretic and semantic origin (linear logic, Scott continuity), but many others are fully open, leaving us wondering about the interactions (or lack thereof) between complexity theory and proof theory/programming languages theory.

10:00-10:25 - Coffee break
Session I: Programs and proofs

Analyzing probabilistic programs with dynamic logic

Tong Cheng (Huazhong University of Science and Technology)

We present a unified framework for the analysis of probabilistic programs based on Dynamic Logic in which both iterative and recursive programs can be analyzed. We augment the traditional rules of probabilistic Dynamic Logic with rules for assignment based on schematic Kleene algebra, as well as proof rules for recursive programs with call-by-value parameters. We show soundness of our system with respect to the standard Markov kernel semantics. We give an example of their use in the analysis of the Coupon Collector’s Problem.


Proof complexity and proof compression via combinatorial flows

Lutz Strassburger (INRIA Saclay --- Ile-de-France)

Combinatorial flows are a novel way of representing proofs in a "syntax-free" way that also includes cut and substitution as proof compression mechanisms. In this paper we show how combinatorial flows are translated into syntactic proofs and vice versa, establishing that combinatorial flows are p-equivalent to Frege systems with substitution.

11:15-12:25 - Break
Session II: Complexity of logical calculi

Discrete temporal constraint satisfaction problems

Manuel Bodirsky (TU Desden), Barnaby Martin (Durham University), Antoine Mottet (Institut fűr Algebra, TU Dresden)

A discrete temporal constraint satisfaction problem is a constraint satisfaction problem (CSP) whose constraint language consists of relations that are first-order definable over the order of the integers. We prove that every discrete temporal CSP is in P, NP-complete, can be formulated as a finite domain CSP.


Filtration versus team semantics

Martin Lück (Leibniz Universität Hannover)

Modal Team Logic (MTL) extends Väänänen's Modal Dependence Logic (MDL) by Boolean negation. Its satisfiability problem is decidable, but the exact complexity is not yet understood very well. We investigate a model-theoretical approach and generalize the successful filtration technique to work in team semantics. We identify an "existential" fragment of MTL that enjoys the exponential model property and is therefore, like Propositional Team Logic (PTL), complete for the class AEXPTIME(poly). Moreover, superexponential filtration lower bounds for different fragments of MTL are proven, up to the full logic having no filtration for any elementary size bound. As a corollary, superexponential gaps of succinctness between MTL fragments of equal expressive power are shown.

12:15-13:45 - Lunch
Session III: Definability

Slicewise definability in first-order logic with bounded quantifier rank

Yijia Chen (Fudan University), Jörg Flum (University of Freiburg), and Xuangui Huang (Shanghai Jiao Tong University)

For every $q\in \mathbb N$ let $\textrm{FO}_q$ denote the class of sentences of first-order logic FO of quantifier rank at most $q$. If a graph property can be defined in $\textrm{FO}_q$, then it can be decided in time $O(n^q)$. Thus, minimizing q has favorable algorithmic consequences. Many graph properties amount to the existence of a certain set of vertices of size $k$. Usually this can only be expressed by a sentence of quantifier rank at least $k$. We use the color-coding method to demonstrate that some (hyper)graph problems can be defined in $\textrm{FO}_q$ where $q$ is independent of $k$. This property of a graph problem is equivalent to the question of whether the corresponding parameterized problem is in the class $\textrm{para-AC}^0$. It is crucial for our results that the FO-sentences have access to built-in addition and multiplication. It is known that then FO corresponds to the circuit complexity class uniform $\textrm{AC}^0$. We explore the connection between the quantifier rank of FO-sentences and the depth of $\textrm{AC}^0$-circuits, and prove that $\textrm{FO}_q \subsetneq \textrm{FO}_{q+1}$ for structures with built-in addition and multiplication.


A complexity theory for implicit graph representations

Maurice Chandoo (Leibniz Universität Hannover)

In an implicit graph representation the vertices of a graph are assigned short labels such that adjacency of two vertices can be algorithmically determined from their labels. This allows for a space-efficient representation of graph classes that have asymptotically fewer graphs than the class of all graphs such as forests or planar graphs. A fundamental question is whether every smaller graph class has such a representation. We consider how restricting the computational complexity of such representations affects what graph classes can be represented. A formal language can be seen as implicit graph representation and therefore complexity classes such as P or NP can be understood as set of graph classes. We investigate this complexity landscape and introduce complexity classes defined in terms of first order logic that capture surprisingly many of the graph classes for which an implicit representation is known. Additionally, we provide a notion of reduction between graph classes which reveals that trees and interval graphs are complete for certain fragments of first order logic in this setting.

14:35-14:45 - Break
14:45-15:45 - Invited talk

A survey on descriptive and implicit characterizations of small complexity classes (invited talk)

Arnaud Durand (Université Denis Diderot - Paris 7)

Descriptive and implicit complexities talk about computational complexity without machines. They offer a logical and algebraic point of view on computational resources that have proved to be fruitful in domain such as database or programming theory.

In this talk, we will survey some methods used to characterize small complexity classes, from the early result of Cobham for polynomial time to more recent ones for circuit classes. We will also consider the more general problem of capturing counting complexity classes and present some new results.

15:45-16:10 - Coffee break
Session IV: Descriptive complexity and deductive formalisms

Characterizing circuit complexity classes by logics with recursion

Anselm Haak (Leibniz Universität Hannover)

We introduce a certain kind of recursion scheme into first-order variants of which allow us to capture a number of classes from circuit complexity, nameley AC1, SAC1, NC1 as well as their counting analogues. The advantage of our new approach is that it allows for a unified characterization of multiple important classes.


Symmetric circuits for rank logic

Anuj Dawar (University of Cambridge), Gregory Wilsenach (University of Cambridge)

Anderson and Dawar (2014) showed that fixed-point logic with counting (FPC) can be characterised by uniform families of polynomial-size symmetric circuits. We give a similar characterisation for fixed-point logic with rank (FPR) by means of symmetric circuits including rank gates. This analysis requires a significant extension of previous methods to deal with gates computing Boolean functions which are not themselves symmetric. In particular, we show that the support theorem of Anderson and Dawar can be extended to circuits whose gates satisfy a property that we term "matrix-symmetry".


An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic

Anupam Das (LIP, ENS Lyon), Patrick Baillot (CNRS, ENS Lyon)

We consider extensions of theories based on the Bellantoni-Cook function algebra for FPTIME by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' arguments and show that the provably total functions are just those of FPH. Our witness extraction proof relies on free-cut elimination in the logic, making use of the witness function method, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FPTIME via the Bellantoni-Cook framework. We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.




We welcome submissions of abstracts based on work submitted or published elsewhere, provided that all pertinent information is disclosed at submission time. There will be no formal reviewing as is usually understood in peer-reviewed conferences with published proceedings. The program committee checks relevance and may provide additional feedback.

Submissions must be in English and in the form of an abstract of about 3-4 pages. All submissions should be submitted through Easychair at:



See the LiCS registration page.


To contact the workshop organizers, please send e-mail to lcc2017@easychair.org.