Calculus captures changing knowledge in logical systems with new framework
Dynamic Proof Theory for Dynamic Epistemic Logic
Logic in Computer Science
Summary
People often want to understand how knowledge changes when events happen, like when new information is shared. The authors developed a new way of writing down logical rules that handle these changes clearly and naturally. Their method uses a structure called dynamic hypersequents with added details about who knows what and what events occurred. This approach guarantees certain logical rules behave nicely and keeps the reasoning process consistent and reliable. It’s the first proof-based system for this kind of logic that works within a common classical framework and also handles changes dynamically.
What this means in practice
- •For security protocol designers: Model and verify knowledge changes in multi-agent systems to ensure protocol correctness under dynamic updates.
- •For interactive game developers: Represent and reason about players' evolving knowledge during gameplay to enable complex information updates.
A theory result. No direct application yet.
Authors
Clara Lerouvillois, Francesca Poggiolesi
Abstract
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.