Speaker
Sam van Gool, Université Paris Cité
Title
Modal Unification Step by Step
Abstract
The unifiability problem for an equational theory asks, given two terms, to decide whether or not there exists a term substitution such that the resulting terms are provably equal in the theory. We propose an approach to unifiability problems in equational theories coming from modal logic, relying on incremental constructions of certain coalgebraic structures that we call "graphs for an endofunctor". We show that, in general, these unifiability problems are effectively equivalent to homomorphism mapping problems from a sequence of such graphs.
We then illustrate this general approach in a number of specific cases, namely: the modal logics K (the logic of all Kripke frames) and Alt1 (the logic of Kripke frames in which every node has at most 1 successor), and a bi-modal logic that we call KdB. In the case of K, we show how our methods give an effective reformulation of the (open) unifiability problem for K into an (also open, but newly identified) decision problem on hypergraphs. For Alt1, the method allows us to establish that the problem is PSPACE-complete. For KdB, we establish that unifiability is equivalent to a homomorphism problem on a sequence of graphs known in the literature as de Bruijn graphs. This talk is based on joint work with Johannes Marti (Universität Zurich), first published in the UNIF 2023 workshop.
