Date: March 27, 2026 (Fri)
Venue: Institute of Science Tokyo, Ookayama Campus, West Area, West Bldg. 8E, 10th Floor
東京科学大学 大岡山キャンパス 西８号館 E棟10階 大会議室
Timetable:
10:30-11:00 Yuki Nishimura: Termination for Hybrid Tableaus via Model Surgery
11:00-11:30 Eiji Yamada: True lies, impossible lies, and iterated announcement
11:30-12:00 Akinori Maniwa: Fully complete transformation from PLL into CS4
13:30-14:00 Ryo Kashima: On cycles in tableaus for modal mu-calculus
14:00-14:30 Yukihiro Oda: Cut-elimination in a cyclic proof system of propositional dynamic logic
14:30-15:00 Leonardo Pacheco: A non-wellfounded proof system for the constructive μ-calculus
15:30-16:00 Yosuke Fukuda: A survey of modal linear logic
16:00-16:30 Yoshihito Tanaka: The models for the common knowledge logic and the provability logic
16:30-17:00 Yoàv Montacute: Reasoning about dynamical systems: from completeness to verification
17:10-17:40 Frank Wolter: Craig Interpolants without Craig Interpolation
Abstract
Yuki Nishimura (Institute of Science Tokyo)
Termination for Hybrid Tableaus via Model Surgery
Hybrid logic extends modal logic by introducing nominals, special propositional symbols that are true at exactly one state in a model. This enhancement increases the expressive power of modal logic, allowing one to define properties of binary relations such as irreflexivity and anti-symmetry—properties not definable in basic modal logic. As a proof system, a complete and terminating tableau calculus for the basic hybrid logic, and later extended this result to the system for the class of transitive models. Today, I introduce some tableau calculi for the class of undirected graphs and for some ordered models, and prove their termination and completeness using methods of model surgery.
Eiji Yamada (University of Tsukuba)
True lies, impossible lies, and iterated announcement
Epistemic logic is the logical study of reasoning about knowledge and belief, and dynamic epistemic logic is the dynamic version of it. In this talk, we will investigate the properties of true lies and impossible lies proposed by Agotnes et al. (2018) as a study in dynamic epistemic logic. Here, a true lie is a lie that becomes true after announced, and an impossible lie is a lie that remains false after announced. We will further introduce their eventual notions and analyze the properties of iterated announcement (i.e., repeatedly announcing the same formula in front of agents).
Akinori Maniwa (Institute of Science Tokyo)
Fully complete transformation from PLL into CS4
Propositional Lax Logic (PLL) and Constructive S4 (CS4) have often been studied in comparison. In this talk, we establish a proof-theoretic relationship by providing syntactic transformations between proofs in both systems. We show that a Fitch-style formulation of CS4 enables a full embedding of PLL in CS4.
Ryo Kashima (Institute of Science Tokyo)
On cycles in tableaus for modal mu-calculus
A tableau system to show validity for modal mu-calculus was introduced by Niwinski-Walukiewicz (1996), where tableaus are infinite tress; they have paths of infinite length. In this talk, we discuss how to finitize the tableaus, using parity automata.
Yukihiro Oda (Tohoku University)
Cut-elimination in a cyclic proof system of propositional dynamic logic
I introduce a cyclic proof system of propositional dynamic logic and show the cut-elimination theorem in it. The theorem is proved semantically by using a finite game.
Leonardo Pacheco (Institute of Science Tokyo)
A non-wellfounded proof system for the constructive μ-calculus
We study μCK, a variant of the modal μ-calculus based on the constructive modal logic CK. We define game semantics for the constructive μ-calculus and use it to prove the soundness and completeness of a non-wellfounded proof system. We also describe how to adapt the game semantics and proof system to the μ-calculus over other non-classical modal logics.
Yosuke Fukuda (Kyoto Tachibana University)
A survey of modal linear logic
In the literature, various systems have been proposed under the name "modal linear logic", each of which integrates modal logic and linear logic in different ways. However, these calculi often differ in their formal properties and underlying motivations. This presentation aims to provide an overview of the existing calculi of modal linear logic to clarify their relationships.
Yoshihito Tanaka (Institute of Science Tokyo / Kyushu Sangyo University)
The models for the common knowledge logic and the provability logic
It is well known that both common knowledge logic and provability logic are complete with respect to (i) the class of Kripke frames satisfying a certain infinitary condition and (ii) the class of modal algebras satisfying the same condition. We show that, in each case, the class of modal algebras determined by the logic does not coincide with this infinitary algebraic class. Moreover, the same phenomenon occurs for every logic axiomatized by ω‑rules. By contrast, on the relational side, the class of Kripke frames determined by common knowledge logic is exactly the class of frames satisfying the infinitary condition, whereas the class of Kripke frames determined by provability logic is a proper superset of that class.
Yoàv Montacute (National Institute of Informatics)
Reasoning about dynamical systems: from completeness to verification
This talk presents a solution to a long-standing open problem posed by Kremer and Mints: a complete axiomatisation for dynamical systems. The approach is based on the Cantor derivative interpretation within the topological semantics of modal logic. Beyond completeness, we examine related logical systems that navigate the tension between expressivity and decidability, and discuss how to adapt these frameworks to make formal verification possible, including recent applications to safety reasoning in autonomous vehicles.
Frank Wolter (University of Liverpool)
Craig Interpolants without Craig Interpolation
A Craig interpolant for formulas A and B is a formula using only the shared non-logical symbols of A and B which is entailed by A and entails B. A logic has the Craig Interpolation Property (CIP) if a Craig interpolant for A and B exists whenever A entails B. Hence the CIP reduces a potentially hard existence problem to an entailment problem. First-order logic, intuitionistic logic, and many modal logics enjoy the CIP. In this talk, I will discuss what happens if a logic does not enjoy the CIP. I will focus on decidability of the interpolant existence problem and on constructing interpolants if they exist. Typical logics without CIP are modal logics with nominal (aka hybrid logics), linear temporal logics, (fragments of) first-order modal logics, and decidable fragments of first-order logic such as the two-variable and guarded fragments. I will discuss a few of these. Often, the interpolant existence problem turns out be one exponential harder than entailment, and sometimes even undecidable for decidable logics.