Synthetic Completeness Proofs for Seligman-style Tableau Systems

Klaus Frovin Jørgensen, Patrick Rowan Blackburn, Thomas Bolander, Torben Braüner

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.
OriginalsprogEngelsk
TitelProceedings of Advances in Modal Logic 2016
RedaktørerLev Beklemishev, Stéphane Demri, András Máté
Vol/bind11
ForlagCollege Publications
Publikationsdato2016
Sider302-321
ISBN (Trykt)978-1-84890-201-5
StatusUdgivet - 2016
BegivenhedAdvances in Modal Logic 2016 - Eotvos University, Budapest, Ungarn
Varighed: 30 aug. 20162 sep. 2016
http://phil.elte.hu/aiml2016/ (Link til konference)

Konference

KonferenceAdvances in Modal Logic 2016
LokationEotvos University
LandUngarn
ByBudapest
Periode30/08/201602/09/2016
Internetadresse

Emneord

  • Hybrid logic
  • difference operator
  • universal modality
  • tense logic
  • pure axioms
  • Bridge rule
  • synthetic completeness method
  • Seligman-style
  • tableaus

Citer dette

Jørgensen, K. F., Blackburn, P. R., Bolander, T., & Braüner, T. (2016). Synthetic Completeness Proofs for Seligman-style Tableau Systems. I L. Beklemishev, S. Demri, & A. Máté (red.), Proceedings of Advances in Modal Logic 2016 (Bind 11, s. 302-321). College Publications.
Jørgensen, Klaus Frovin ; Blackburn, Patrick Rowan ; Bolander, Thomas ; Braüner, Torben. / Synthetic Completeness Proofs for Seligman-style Tableau Systems. Proceedings of Advances in Modal Logic 2016. red. / Lev Beklemishev ; Stéphane Demri ; András Máté. Bind 11 College Publications, 2016. s. 302-321
@inproceedings{be2316063b7f47a397ee4507732a871a,
title = "Synthetic Completeness Proofs for Seligman-style Tableau Systems",
abstract = "Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.",
keywords = "Hybrid logic, difference operator, universal modality, tense logic, pure axioms, Bridge rule, synthetic completeness method, Seligman-style, tableaus",
author = "J{\o}rgensen, {Klaus Frovin} and Blackburn, {Patrick Rowan} and Thomas Bolander and Torben Bra{\"u}ner",
year = "2016",
language = "English",
isbn = "978-1-84890-201-5",
volume = "11",
pages = "302--321",
editor = "Lev Beklemishev and St{\'e}phane Demri and Andr{\'a}s M{\'a}t{\'e}",
booktitle = "Proceedings of Advances in Modal Logic 2016",
publisher = "College Publications",

}

Jørgensen, KF, Blackburn, PR, Bolander, T & Braüner, T 2016, Synthetic Completeness Proofs for Seligman-style Tableau Systems. i L Beklemishev, S Demri & A Máté (red), Proceedings of Advances in Modal Logic 2016. bind 11, College Publications, s. 302-321, Advances in Modal Logic 2016, Budapest, Ungarn, 30/08/2016.

Synthetic Completeness Proofs for Seligman-style Tableau Systems. / Jørgensen, Klaus Frovin; Blackburn, Patrick Rowan; Bolander, Thomas; Braüner, Torben.

Proceedings of Advances in Modal Logic 2016. red. / Lev Beklemishev; Stéphane Demri; András Máté. Bind 11 College Publications, 2016. s. 302-321.

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Synthetic Completeness Proofs for Seligman-style Tableau Systems

AU - Jørgensen, Klaus Frovin

AU - Blackburn, Patrick Rowan

AU - Bolander, Thomas

AU - Braüner, Torben

PY - 2016

Y1 - 2016

N2 - Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.

AB - Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.

KW - Hybrid logic

KW - difference operator

KW - universal modality

KW - tense logic

KW - pure axioms

KW - Bridge rule

KW - synthetic completeness method

KW - Seligman-style

KW - tableaus

M3 - Article in proceedings

SN - 978-1-84890-201-5

VL - 11

SP - 302

EP - 321

BT - Proceedings of Advances in Modal Logic 2016

A2 - Beklemishev, Lev

A2 - Demri, Stéphane

A2 - Máté, András

PB - College Publications

ER -

Jørgensen KF, Blackburn PR, Bolander T, Braüner T. Synthetic Completeness Proofs for Seligman-style Tableau Systems. I Beklemishev L, Demri S, Máté A, red., Proceedings of Advances in Modal Logic 2016. Bind 11. College Publications. 2016. s. 302-321