Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Update Logic

Guillaume Aucher 1 
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We introduce a two-sorted substructural logic called 'Update Logic' where the central objects of study are updates, which are represented formally by ternary relations. We develop a basic correspondence theory which relates properties of ternary relations with axioms and inference rules stating properties of updates. We claim that update logic can capture various logic-based formalisms dealing with belief change. As case study, we consider the logical framework of Dynamic Epistemic Logic (DEL) and we show that we can embed it within update logic. Also, we identify axioms and inference rules that completely characterize the DEL product update. Moreover, we introduce Gentzen calculi which extend Gentzen calculi for modal logic and which axiomatize our update logic and DEL. Our completeness proof techniques are new compared to the standard proof techniques used to prove completeness of Gentzen calculi. Our contributions to proof theory are independent from our contributions to the study of logical dynamics and can also be read independently.
Complete list of metadata

Cited literature [84 references]  Display  Hide  Download
Contributor : Guillaume Aucher Connect in order to contact the contributor
Submitted on : Thursday, August 1, 2013 - 12:39:16 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:08 AM
Long-term archiving on: : Wednesday, April 5, 2017 - 6:56:51 PM


Files produced by the author(s)


  • HAL Id : hal-00849856, version 1


Guillaume Aucher. Update Logic. [Research Report] RR-8341, INRIA. 2013. ⟨hal-00849856⟩



Record views


Files downloads