Displaying Updates in Logic

Guillaume Aucher 1, 2
2 LIS - Logical Information Systems
IRISA-D7 - GESTION DES DONNÉES ET DE LA CONNAISSANCE
Abstract : We generalize the language of substructural logics interpreted over the ternary relational semantics. This is motivated by our intention to capture within the logical framework of substructural logics various logic-based formalisms dealing with common sense reasoning and logical dynamics. This initiative is based on the key observation that an update can be represented abstractly by the ternary relation of the substructural framework: the first argument of the ternary relation represents an initial situation, the second an informative event and the third the resulting situation after the occurrence of the informative event. Refining the language of substructural logics may allow us to account for the fine-grained reasoning present in common sense reasoning. Thus, we introduce three triples of connectives that are interconnected by means of cyclic permutations. The usual fusion, implication and co-implication connectives form one of these triples. We define a cut-free display calculus for our language that generalizes the display calculus for modal logic. We do not resort to structural connectives for truth constants and we show how we can obtain our display rules using Gaggle Theory. We prove the soundness and strong completeness of our display calculus via a Henkin-style construction. Using correspondence results from substructural logics, we also obtain sound and complete display calculi for a wide variety of classical and substructural logics. Then, we define dual substructural connectives and we provide a display calculus for our language extended with these dual connectives. Finally, we focus on the specific case of bi-intuitionistic logic for which we provide a novel sound and strongly complete display calculus. In a companion article (Aucher, 2016, J. Logic Comput.), we provide a sequent calculus for update logic that generalizes the non-associative Lambek calculus and a sequent calculus for dynamic epistemic logic that extends this sequent calculus for update logic.
Type de document :
Article dans une revue
Journal of Logic and Computation, Oxford University Press (OUP), 2016, 26 (6), pp.1865-1912. 〈10.1093/logcom/exw001〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01476234
Contributeur : Guillaume Aucher <>
Soumis le : samedi 8 avril 2017 - 10:47:37
Dernière modification le : jeudi 15 novembre 2018 - 11:57:37
Document(s) archivé(s) le : dimanche 9 juillet 2017 - 12:32:49

Fichier

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

Identifiants

Citation

Guillaume Aucher. Displaying Updates in Logic. Journal of Logic and Computation, Oxford University Press (OUP), 2016, 26 (6), pp.1865-1912. 〈10.1093/logcom/exw001〉. 〈hal-01476234〉

Partager

Métriques

Consultations de la notice

1021

Téléchargements de fichiers

76