Embedded Files
Speaker: Lutz Strassburger
Title: Intuitionistic S4 is decidable
Abstract: In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson’s PhD thesis in 1994. We obtain this result by performing proof search in a labeled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.
Relevant Papers:
Intuitionistic S4 is decidable, LICS 2023 https://arxiv.org/pdf/2304.12094
A Simple Loopcheck for Intuitionistic K, WoLLIC 2024 https://inria.hal.science/hal-04569308v1/file/main-nocomment.pdf
Speaker: Pablo Barcelo
Title: The Role of Logic in Advancing Machine Learning: Three Case Studies
Abstract: I present three case studies from my collaborative research that highlight the essential role of logic in enhancing our understanding of modern machine learning architectures. The first two examples focus on the expressive capabilities of two prominent architectures: Transformers, which have revolutionized NLP applications, and Graph Neural Networks, a leading approach for classifying graph-structured data. We employ temporal logic techniques to analyze the properties that Transformers can recognize, and modal logics to examine the properties discernible by Graph Neural Networks. The third example addresses the pursuit of explainable AI, demonstrating how first-order logic can be used to design languages that declare, evaluate, and compute explanations for decisions made by machine learning models.
Relevant Papers:
Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan L. Reutter, Juan Pablo Silva: The Logical Expressiveness of Graph Neural Networks. ICLR 2020 https://hal.science/hal-03356968/document
Logical Languages Accepted by Transformer Encoders with Hard Attention. Pablo Barcelo, Alexander Kozachinskiy, Anthony Widjaja Lin, Vladimir Podolskii. ICLR 2024 https://arxiv.org/abs/2310.03817
Marcelo Arenas, Pablo Barceló, Diego Bustamente, Jose Caraball, Bernardo Subercaseaux: A Symbolic Language for Interpreting Decision Trees. CoRR abs/2310.11636 (2023)
Speaker: Alexander Kozachinskiy
Title: Memory-less strategies in games on graphs.
Abstract: We consider games on graphs where two players are moving a token along edges of the graph for infinitely many turns. We are studying which winning conditions are memory-less determined, meaning that in every graph one of the players has a memory-less winning strategy (the moves do not depend on the history).
I will present a ``cleaned up'' exposition of an old result of Gimbert and Zielonka (CONCUR'05), saying that for a winning condition to be memory-less determined, it is enough to be so in ``degenerate games'', where there is only one of the players making moves. This result easily implies memory-less determinacy of parity and mean-payoff games.
Relevant Paper:
Hugo Gimbert and Wieslaw Zielonka, Games where you can play optimally without any memory. CONCUR 05 (pdf).
Speakers: Mario Benevides and Bruno Lopes
Title: Towards expressiveness and complexity in Propositional Dynamic Logic (or controlling the complexity Vs enhancing expressiveness)
Abstract: Propositional Dynamic logic is a sophisticated modal logic tailored to reason about programs. Several worth-of-studying fragments (controlling the complexity) and extensions (aiming to increase expressiveness) exist. We discuss some impacts of restricting to deterministic programs and how to enhance expressiveness using memory.
The first approach relies on the usage of Guarded Kleene Algebras with Tests (GKAT) to define Strict Deterministic PDL programs (which will compose GPDL). As GKAT programs can be translated to Thompson's Automata and have its equivalence determined in almost linear time, the proposed algorithm is used to show that in GPDL $\models\langle\pi\rangle p \leftrightarrow \langle\eta\rangle p \Leftrightarrow \pi = \eta$.
A second approach consists of increasing the expressiveness by adding a memory to PDL. Differently from typical Memory Logics, the memory is in the syntax and not only in the model. We show that it is possible to reason about some context-sensitive languages and, for bounded memory, present a [factorial] translation to standard PDL.
Relevant Papers:
Mario Benevides, Leandro Gomes, Bruno Lopes. Towards determinism in PDL: relations and proof theory. Journal of Logic and Computation, Oxford, UK, 2024.
Mario Benevides, Bruno Lopes. Memory Propositional Dynamic Logic. In: Edward Hermann Haeusler, Luiz Carlos Pinheiro Dias Pereira, Jorge Petrucio Viana. (Org.). A Question is More Illuminating than an Answer. A Festschrift for Paulo A. S. Veloso. 1ed. College Publications, Oxford, UK, 2021 (pdf)
Speaker: Juan Reutter
Title: Cardinality estimation and distributed computation of graph queries
Abstract: In this talk I will present two different, recent results about graph queries: a way of estimating the cardinality of graph patterns featuring path queries, that extends the AGM bound, and communication bounds for the federated computation of graph pattern queries. These results are important in the development of efficient graph database systems, and should open up new avenues for studying other forms of query—or logical— languages.
Relevant Papers:
Communication Cost of Joins over Federated Data, in ICDT 2024, with Tamara Cucumides, U Antwerp. Communication Cost of Joins over Federated Data
Size Bounds and Algorithms for Conjunctive Regular Path Queries, in ICDT 2023, with Tamara Cucumides, U Antwerp and Domagoj Vrgoc, PUC Chile. Size Bounds and Algorithms for Conjunctive Regular Path Queries
Speaker: Carlos Areces
Title: Axiomatizing Dynamic Logics without Substitution
Abstract: Modal logics with dynamic operators (e.g., operators that can update edges anywhere in the model) are usually very expressive. Their satisfiability problem is usually undecidable, and model checking is PSpace-complete. Axiomatizing their validities is also challenging, as they are usually not closed under uniform substitution. A recent paper shows a new approach to this last problem, using hybrid logics. I will discuss some details of this construction.
Relevant Paper:
van Benthem, J.; Li, L.; Shi, C.; and H. Yin. (2022) Hybrid sabotage modal logic. Journal of Logic and Computation, 33(6):1216–1242.
Speaker: Raul Fervari
Title: Reasoning with Constrained Ability-Based Logics: from Tractability to Ack-Completeness
Abstract: We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of “knowing how”. We consider the most standard ability based knowing-how logic, for which we show that model-checking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATL-like logics. We show that for the former logic enriched with budgets, the complexity increases to Ack-completeness, whereas for the latter, the PTime bound is preserved.
Relevant Paper:
Stéphane Demri and Raul Fervari. Model-Checking for Ability-Based Logics with Constrained Plans. 37th AAAI Conference on Artificial Intelligence (AAAI-23), volume 37, number 5, pages 6305-6312, 2023. https://cs.famaf.unc.edu.ar/~rfervari/files/papers/2023-aaai.pdf
Speaker: Valentin Cassano
Title: Nonmonotonic Reasoning via Dynamic Consequence
Abstract: We approach the concept of Pivotal Rule Consequence (𝖯𝖱𝖢) from a semantical perspective, resorting to model updates in Public Announcement Logic (𝖯𝖠𝖫). In doing this, we take inspiration from the notion of dynamic consequence. Our perspective gains in interest since 𝖯𝖱𝖢 serves as a “bridge” from Classical Logic to Default Logic –one of the most well-known non-monotonic formalisms. We show how the internalization of 𝖯𝖱𝖢 in 𝖯𝖠𝖫 leads to clear semantics of the former, and to completeness and transfer results. Moreover, we address the case of credulous consequence in Default Logic as a particular case of 𝖯𝖱𝖢. Interestingly, we cast credulous consequence as a model checking problem. We argue that our results open the way to use well-known semantic tools from modal logic to study properties of different non-monotonic logics.
Relevant Paper:
C. Areces, V. Cassano, R. Fervari: Non-monotonic Reasoning via Dynamic Consequence. WoLLIC 2022: 395-410 https://vcassano.github.io/assets/pdf/wolllic2020.pdf
Speaker: Danae Dutto
Title: Proof Theory for Data-Aware Modal Logics.
Abstract: Data-aware modal languages have received considerable attention lately. The interest rose from the formal study of database-oriented languages like DataGL, XPath and GQL. These modal languages, in addition to reachability statements, can describe properties about data (e.g., data comparisons). A well-rounded example of this kind of language is HXPathD introduced in [10]. HXPathD is a hybrid modal language formalizing the navigational fragment of XPath enriched with data comparisons, labels for nodes (keys), and jump-to-key operators. The main results in [10] include a strongly complete Hilbert-style axiomatization for HXPathD , and extensions characterizing various classes of models of interest. Adding to these results, in this article, we take the first steps towards a proof theory for HXPathD , and more generally, for data-aware modal logics. Concretely, we present a sound, complete, and cut free Gentzen-style sequent calculus for HXPathD , and study its properties.
Relevant Paper:
C. Areces, V. Cassano, D. Dutto, and R. Fervari, Sequent Calculi for Data-Aware Modal Logics.
Page updated
Google Sites
Report abuse