arXiv subjects

Clara Lerouvillois

Publications and source records attributed to Clara Lerouvillois.

4 recordsLinked to original sources

arXiv2026

Dynamic Proof Theory for Dynamic Epistemic Logic

This paper proposes a calculus for Dynamic Epistemic Logic (DEL) based on dynamic hypersequents, a new framework for capturing the dynamics of epistemic models in a purely structural and natural way. We enrich dynamic hypersequents with agent indices and an event store, yielding a uniform representation of epistemic events. The resulting calculus enjoys a set of logical rules that are provably invertible. Moreover, all structural rules, including the contraction rules, as well as the cut-rule, are shown to be admissible. Finally, the calculus constitutes, to the best of our knowledge, the only proof-theoretic calculus for DEL that is both grounded in a classical S5 framework and inherently dynamic.

cs.LO↗

arXiv2026

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

cs.LO↗

arXiv2026

Resolving Asynchronous Distributed Knowledge

There are by now various epistemic modal logics with intersection modalities for distributed knowledge and intersection update modalities for dynamic phenomena like agents sharing (all their) information, agents receiving information from other agents, and full information protocols. One of those is the logic of Resolving Distributed Knowledge, by Agotnes and Wang. It has distributed knowledge modalities for arbitrary subsets of the set of all agents and it also has so-called resolution modalities for arbitrary subsets of agents sharing their knowledge. In that logic, the agents not involved in the knowledge sharing are aware of the agents sharing knowledge, agents are memory-less, and the kind of dynamics represents synchronous updates, where there is common awareness of the global clock. In contrast, in this contribution we present a logic for Resolving Asynchronous Distributed Knowledge. It is an asynchronous generalization of the synchronous logic of resolving distributed knowledge. The logical semantics is history-based: truth is not only with respect to a given world in a model, but also with respect to a given history of prior resolutions, of which each individual agent can only observe a part. In particular, an agent is unaware of resolutions for groups of agents not including her. As is to be expected, this comes with many technical complications, for example concerning the axiomatization. The synchronous axioms relating resolution to distributed knowledge are now invalid. The modelling advantages of such an asynchronous novel logic, for distributed computing and similar areas, are however substantial and a major asset.

cs.LO↗

arXiv2026

Dynamic Hypersequents for Public Announcement Logic

Dynamic Epistemic Logic extends classical epistemic logic by modeling not only static knowledge but also its evolution through information updates. Among its various systems, Public Announcement Logic (PAL) provides one of the simplest and most studied frameworks for representing epistemic change. While the semantics of PAL is well understood as transformation of Kripke models, the proof theory so far developed fails to represent this dynamism in purely syntactical terms. In this paper we propose a step toward addressing this gap. In particular, building on a hypersequent calculus for S5, we extend it with a mechanism that models the transition between epistemic models induced by public announcements. We call these structures dynamic hypersequents. Using dynamic hypersequents, we construct a calculus for PAL and we show that it enjoys several desirable properties: admissibility of all structural rules (including contraction), invertibility of logical rules, as well as syntactic cut-elimination.

cs.LO↗