Summary of the talks

Speaker: Lutz Strassburger

Title: An Introduction to Combinatorial Proofs

Abstract: Combinatorial proofs, also known as  “proofs without syntax”, form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. This is achieved by factoring a proof into a purely linear proof and a resource management part. In the talk, I will present the basic ideas behind combinatorial proofs and present combinatorial proofs for classical logic and, if time permits, also for intuitionistic logic.

The talk will be based on many papers, some of them joint with Dominic Hughes and Willem Heijltjes, and with Matteo Acclavio. A good resource are the lecture notes for the ESSLLI 2021 course: https://inria.hal.science/hal-03316571

Speaker: Dietmar Berwanger

Title: The Dynamics of Information: What to Know, What to Forget

Abstract: Reactive processes operate in an ongoing dialogue with their environment: at each step, they observe an input and respond with a control action, with the purpose of fulfilling a global objective. Unlike terminating programs, they are meant to run indefinitely. This raises fundamental questions about how information should be stored, transmitted or discarded. A second layer of complexity arises in distributed settings, where processes have only partial knowledge of the global state and must coordinate under information constraints.

In the talk, I will discuss recent results on how infinite streams of input can be represented and managed to support strategic coordination. We will explore the roles of memory and signalling in distributed decision-making, as well as the extremal case of full-information protocols. 

The presentation is based on joint work with Patricia Bouyer, Laurent Doyen, and Thomas Soullard.

Speaker: Mario Benevides

Title: Graphs, Complexity and Modal Logics

Abstract: In this talk, we will present how problems of computational complexity can be approached using logics. In particular, we will present a series of results involving graph classes and modal logics. We will also touch a bit on descriptive complexity, but always with a focus on modal logics.

Speaker: Danae Dutto

Title: Proof Theory for Hybrid Logics

Abstract: Hybrid logics extend classical modal logics by adding a limited form of equality reasoning. This additional expressive power yields a strong model theory, with well-known results such as strong completeness for axiomatic systems extended by pure axioms. On the proof-theoretic side, hybrid logics have been studied from different perspectives (see, e.g., Torben, 2011; Indrzejczak, 2020), yet their connections with labelled sequent calculi remain not fully understood. In this talk, I will present ongoing work exploring these connections, focusing in particular on the relationship between sequent calculi for hybrid logics and Negri’s labelled systems for modal logics with equality. I will also discuss some preliminary findings regarding rule invertibility and cut elimination.

Speaker: Anouk Oudshoorn

Title: SHACL Satisfiability: What Can We Learn from DLs?

Abstract: Since the introduction of the SHACL standard, understanding its computational features and formal foundations has become essential. Some research has focused on the semantics of recursive constraints and the complexity of validation, but the satisfiability of SHACL constraints remains largely unexplored. The most significant previous work in this direction is rather coarse, obtaining very few positive results for finite satisfiability and for fragments with counting. In this talk, I build on description logics to paint a comprehensive and fine-grained boundary for SHACL fragments with a decidable satisfiability problem under the supported semantics, both for unrestricted and finite models.

Speaker: Alexander Kozachinskiy

Title: Gödel's incompleteness and Kolmogorov complexity

Abstract: The first Gödel's incompleteness theorem states that if ZFC is not contradictory, then there is a statement phi such that neither phi nor its negation can be proved in ZFC. The second Gödel's incompleteness theorem states that as such statement phi you can take a statement ``ZFC is not contradictory''. Kolmogorov complexity gives an interesting perspective on these results. It is not hard to prove the first theorem for phi that encodes so-called Berry paradox using Kolmogorov complexity. Moreover, Kritchman and Raz have demonstrated how prove the second theorem using ``surprise examination paradox'' and Kolmogorov complexity. I will try to explain these results.

This is joint work with A. Shen and B. Bauwens. 

Speaker: Miguel Romero

Title: Minimizing Conjunctive Regular Path Queries

Abstract: We study the minimization problem for Conjunctive Regular Path Queries (CRPQs) and unions of CRPQs (UCRPQs). This is the problem of checking, given a query and a number k, whether the query is equivalent to one of size at most k. For CRPQs we consider the size to be the number of atoms, and for UCRPQs the maximum number of atoms in a CRPQ therein, motivated by the fact that the number of atoms has a leading influence on the cost of query evaluation. We show that the minimization problem is decidable, both for CRPQs and UCRPQs. We provide a 2ExpSpace upper-bound for CRPQ minimization, based on a brute-force enumeration algorithm, and an ExpSpace lower-bound. For UCRPQs, we show that the problem is ExpSpace-complete, having thus the same complexity as the classical containment problem. The upper bound is obtained by defining and computing a notion of maximal under-approximation. Moreover, we show that for UCRPQs using the so-called simple regular expressions consisting of concatenations of expressions of the form a+ or a1 + ⋅⋅⋅ + ak, the minimization problem becomes "Pi_2ˆP"-complete, again matching the complexity of containment.

Speaker: Antonio Mondejar

Title: Computational Aspects of Bisimulations for a Logic of Knowing How

Abstract: We investigate computationals aspects related to the notion of bisimulation in the context of an uncertainty-based knowing how logic. First, we introduce a new definition for such a notion, so that only purely structural characteristics of the models are required and we show the desired adequacy results for this new definition. Then, we study the computational complexity of some classical problems regarding this new definition; in particular, we proved that the problem of deciding whether two models are bisimilar is coNP-complete and that this is also the case for the pointed version of this problem. Lastly, we investigate bisimulation-based model contractions in order to obtain minimal models under some particular size measure. Moreover, we establish 

that our proposal for model contraction can be computed in polynomial time.

This presentation is based on joint work with Raul Fervari and Carlos Areces.