Common knowledge: finite calculus with a syntactic cut-elimination procedure - HAL-SHS - Sciences de l'Homme et de la Société Accéder directement au contenu
Article Dans Une Revue Logique et Analyse Année : 2015

Common knowledge: finite calculus with a syntactic cut-elimination procedure

Résumé

In this paper we present a finitary sequent calculus for the S5 multi-modal system with common knowledge. The sequent calculus is based on indexed hypersequents which are standard hypersequents refined with indices that serve to show the multi-agent feature of the system S5. The calculus has a non-analytic right introduction rule. We prove that the calculus is contraction- and weakening-free, that (almost all) its logical rules are invertible, and finally that it enjoys a syntactic cut-elimination procedure. Moreover, the use of the non-analytic rule can be restricted so that the calculus can be considered as suitable for proof search.

Mots clés

Fichier principal
Vignette du fichier
commonknoweldgefinal.pdf (150.22 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

halshs-00775822 , version 1 (21-04-2016)

Identifiants

  • HAL Id : halshs-00775822 , version 1

Citer

Brian Hill, Francesca Poggiolesi. Common knowledge: finite calculus with a syntactic cut-elimination procedure. Logique et Analyse, 2015, 58 (230), pp.279-306. ⟨halshs-00775822⟩
247 Consultations
277 Téléchargements

Partager

Gmail Facebook X LinkedIn More