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 metadatas

Cited literature [84 references]  Display  Hide  Download

https://hal.inria.fr/hal-00849856
Contributor : Guillaume Aucher <>
Submitted on : Thursday, August 1, 2013 - 12:39:16 PM
Last modification on : Friday, November 16, 2018 - 1:30:29 AM
Long-term archiving on : Wednesday, April 5, 2017 - 6:56:51 PM

File

RR8341.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00849856, version 1

Citation

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

Share

Metrics

Record views

575

Files downloads

183