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