Logic and Computational Complexity

An International Workshop Series


 

LCC'22 MEETING

The Twenty Second International Workshop on Logic and Computational Complexity will be held online on February 20, 2022, collocated with CSL 2022

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.

IMPORTANT DATES

Workshop: February 20, 2022

Registration

Registration to the workshop is free but needs to be done on the CSL'22 registration page in order to receive updates and links for the online programme.

INVITED SPEAKERS

CONTRIBUTED TALKS

  • Peter Hines. The combinatorics of some category theory underlying Girard's Geometry of Interaction program
  • Benedikt Pago. Deciding Graph Non-Isomorphism in Deep Weisfeiler Leman, Choiceless Polynomial Time, and the Extended Polynomial Calculus
  • Gianluca Curzi and Anupam Das. Cyclic Implicit Complexity
  • Nancy Abigail Nuñez Hernandez. The scandal of deduction and the complexity of Logical Entailment
  • Michal Gajda. Consistent ultrafinitist logic
  • Damiano Mazza. A Functorial Approach to Structural Complexity Theory

PROGRAM COMMITTEE

  • Patrick Baillot (CNRS, University of Lille, France, co-chair)
  • Meghyn Bienvenu (CNRS, University of Bordeaux, France)
  • Juha Kontinen (University of Helsinki, Finland, co-chair)
  • Cynthia Kop (Radboud University Nijmegen, The Netherlands)
  • Barnaby Martin (Durhan University, UK)
  • Nicole Schweikardt (Humboldt-University Berlin, Germany)

LCC 2022 Schedule (all times in CET)

09:20 - 09:30
Welcome
09:30 - 10:10
Invited speaker: Stephan Kreutzer. Dense Model-Checking (abstract below)
10:10 - 10:30
Benedikt Pago. Deciding Graph Non-Isomorphism in Deep Weisfeiler Leman, Choiceless Polynomial Time, and the Extended Polynomial Calculus
10:30-11:00
Break
11:00-11:40
Invited speaker: Carsten Lutz. Enumerating Answers to Ontology-Mediated Queries (abstract below)
11:40-12:00
Nancy Abigail Nuñez Hernandez. The scandal of deduction and the complexity of Logical Entailment

12:00-13:30
Lunch Break

13:30-14:10
Invited speaker: Isabel Oitavem. The Polynomial Hierarchy of Functions Revisited
14:10-14:30
Gianluca Curzi and Anupam Das. Cyclic Implicit Complexity
14:30-15:00
Break
15:00-15:20
Damiano Mazza. A Functorial Approach to Structural Complexity Theory
15:20-15:40
Peter Hines. The combinatorics of some category theory underlying Girard's Geometry of Interaction program
15:40-16:00
Michal Gajda. Consistent ultrafinitist logic
16:00-16:10
Closing

Abstracts of invited talks

Stephan Kreutzer. Dense Model-Checking
Algorithmic meta-theorems aim to explain the tractability of entire families of problems that can be specified in some logic. The prime example is Courcelle's theorem, stating that every problem expressible in monadic second-order logic (MSO) can be solved in linear time on every class of graphs with bounded tree-width. In other words, the model-checking problem for MSO is fixed-parameter tractable on every class of graphs of bounded tree-width. Following Courcelle's theorem, the focus of this line of research has shifted to model-checking for first-order logic (FO). The primary goal of a long line of research on algorithmic meta-theorems is to identify structural properties of classes of graphs or structures which precisely characterise those classes of graphs on which model-checking for first-order logic is fixed-parameter tractable. This question has been answered for sparse classes of graphs, that is, classes which are closed under taking subgraphs, by Grohe, Siebertz and Kreutzer in 2015: FO model-checking is fixed-parameter tractable on any such class C if, and only if, C is nowhere dense. The analogous question for dense classes of graphs is still wide open. In this talk I will first give a general introduction into this field and review some of the main results. The focus of the second part of the talk will then be on current developments in the area of FO-model-checking on dense classes of graphs. In particular I will present some very recent progress that has been made towards pushing the tractability boundary for FO on dense graphs.

Carsten Lutz. Enumerating Answers to Ontology-Mediated Queries
Ontology-mediated querying is an approach to querying incomplete data where an ontology is used to inject domain knowledge, often enabling more complete answers to queries. In this presentation, I report about recent results about enumerating answers to ontology- mediated queries with linear preprocessing and constant delay. In particular, I will consider ontologies formalized as sets of guarded TGDs and answers that may involve wildcards.

CONTACT

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