Cut-free display calculi for nominal tense logics

Stéphane Demri; Rajeev Goré

doi:10.1007/3-540-48754-9_16

Cut-free display calculi for nominal tense logics

Stéphane Demri, Rajeev Goré

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

8 Citations (Scopus)

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’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.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings
Editors	Neil V. Murray
Publisher	Springer Verlag
Pages	155-170
Number of pages	16
ISBN (Print)	3540660860, 9783540660866
DOIs	https://doi.org/10.1007/3-540-48754-9_16
Publication status	Published - 1999
Event	International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999 - Saratoga Springs, United States Duration: 7 Jun 1999 → 11 Jun 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1617
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999
Country/Territory	United States
City	Saratoga Springs
Period	7/06/99 → 11/06/99

Access to Document

10.1007/3-540-48754-9_16

Cite this

Demri, S., & Goré, R. (1999). Cut-free display calculi for nominal tense logics. In N. V. Murray (Ed.), Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings (pp. 155-170). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1617). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_16

Demri, Stéphane ; Goré, Rajeev. / Cut-free display calculi for nominal tense logics. Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings. editor / Neil V. Murray. Springer Verlag, 1999. pp. 155-170 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Demri, S & Goré, R 1999, Cut-free display calculi for nominal tense logics. in NV Murray (ed.), Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1617, Springer Verlag, pp. 155-170, International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999, Saratoga Springs, United States, 7/06/99. https://doi.org/10.1007/3-540-48754-9_16

Cut-free display calculi for nominal tense logics. / Demri, Stéphane; Goré, Rajeev.
Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings. ed. / Neil V. Murray. Springer Verlag, 1999. p. 155-170 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1617).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Cut-free display calculi for nominal tense logics

AU - Demri, Stéphane

AU - Goré, Rajeev

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84957372361&partnerID=8YFLogxK

U2 - 10.1007/3-540-48754-9_16

DO - 10.1007/3-540-48754-9_16

M3 - Conference contribution

SN - 3540660860

SN - 9783540660866

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 155

EP - 170

BT - Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings

A2 - Murray, Neil V.

PB - Springer Verlag

T2 - International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1999

Y2 - 7 June 1999 through 11 June 1999

ER -

Demri S, Goré R. Cut-free display calculi for nominal tense logics. In Murray NV, editor, Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1999, Proceedings. Springer Verlag. 1999. p. 155-170. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48754-9_16

Cut-free display calculi for nominal tense logics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this