@inproceedings{69e7ec9c241f4f78b69414d49e53715d,
title = "Cut-free display calculi for nominal tense logics",
abstract = "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{\textquoteright}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{\textquoteright}s condition (C8), we extend Wansing{\textquoteright}s strong normalisation theorem to get a similar theorem for any extension of δMNTL by addition of structural rules satisfying Belnap{\textquoteright}s conditions (C2)-(C7). Finally, we show a weak Sahlqvist-style theorem for extensions of MNTL, and by Kracht{\textquoteright}s techniques, deduce that these Sahlqvist extensions of δMNTL also admit cut-free display calculi.",
author = "St{\'e}phane Demri and Rajeev Gor{\'e}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999 ; Conference date: 07-06-1999 Through 11-06-1999",
year = "1999",
doi = "10.1007/3-540-48754-9\_16",
language = "English",
isbn = "3540660860",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "155--170",
editor = "Murray, \{Neil V.\}",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings",
address = "Germany",
}