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.
Liste complète des métadonnées

Littérature citée [84 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00849856
Contributeur : Guillaume Aucher <>
Soumis le : jeudi 1 août 2013 - 12:39:16
Dernière modification le : mercredi 16 mai 2018 - 11:23:04
Document(s) archivé(s) le : mercredi 5 avril 2017 - 18:56:51

Fichier

RR8341.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00849856, version 1

Citation

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

Partager

Métriques

Consultations de la notice

561

Téléchargements de fichiers

179