Cut-Free Display Calculi for Nominal Tense Logics - IMAG Accéder directement au contenu
Communication Dans Un Congrès Année : 1999

Cut-Free Display Calculi for Nominal Tense Logics

Résumé

We define cut-free display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use a translation of MNTL into the minimal tense logic of inequality (MTL≠) which is known to be properly displayable by application of Kracht’s results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δMTL≠ for MTL≠. Since δMNTL does not satisfy Belnap’s condition (C8), we extend Wansing’s strong normalisation theorem to get a similar theorem for any extension of δMNTL by addition of structural rules satisfying Belnap’s conditions (C2)–(C7). Finally, we show a weak Sahlqvist-style theorem for extensions of MNTL, and by Kracht’s techniques, deduce that these Sahlqvist extensions of δMNTL also admit cut-free display calculi.
Fichier principal
Vignette du fichier
final-demrigore-tab99.pdf (349.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03201530 , version 1 (19-04-2021)

Identifiants

Citer

Stéphane Demri, Rajeev Goré. Cut-Free Display Calculi for Nominal Tense Logics. Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '99, Saratoga Springs, NY, Neil Murray, Jun 1999, Saratoga Springs, United States. pp.155-170, ⟨10.1007/3-540-48754-9_16⟩. ⟨hal-03201530⟩

Collections

UGA IMAG CNRS
23 Consultations
63 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More