Synthetic Completeness for a Terminating Seligman-Style Tableau System

Asta Halkjær From

doi:10.4230/LIPIcs.TYPES.2020.5

Synthetic Completeness for a Terminating Seligman-Style Tableau System

Asta Halkjær From

Department of Applied Mathematics and Computer Science

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

42 Downloads (Pure)

Abstract

Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.

Original language	English
Title of host publication	Proceedings of 26^th International Conference on Types for Proofs and Programs
Publisher	Schloß Dagstuhl
Publication date	2021
Pages	5:1--5:17
ISBN (Print)	978-3-95977-182-5
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2020.5
Publication status	Published - 2021
Event	26^th International Conference on Types for Proofs and Programs - University of Turin, Turin, Italy Duration: 2 May 2020 → 5 May 2020 https://types2020.di.unito.it/

Conference

Conference	26^th International Conference on Types for Proofs and Programs
Location	University of Turin
Country/Territory	Italy
City	Turin
Period	02/05/2020 → 05/05/2020
Internet address	https://types2020.di.unito.it/

Series	Leibniz International Proceedings in Informatics
Volume	188
ISSN	1868-8969

Keywords

Hybrid logic
Seligman-style tableau
Synthetic completeness
Isabelle/HOL

Access to Document

10.4230/LIPIcs.TYPES.2020.5

FulltextFinal published version, 817 KB

OpenUrl availability

Full text

Cite this

@inproceedings{0172c97e21d84c8eb9b281f950e12f45,

title = "Synthetic Completeness for a Terminating Seligman-Style Tableau System",

abstract = "Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.",

keywords = "Hybrid logic, Seligman-style tableau, Synthetic completeness, Isabelle/HOL",

author = "From, {Asta Halkj{\ae}r}",

year = "2021",

doi = "10.4230/LIPIcs.TYPES.2020.5",

language = "English",

isbn = "978-3-95977-182-5",

series = "Leibniz International Proceedings in Informatics",

publisher = "Schlo{\ss} Dagstuhl",

pages = "5:1----5:17",

booktitle = "Proceedings of 26th International Conference on Types for Proofs and Programs",

note = "26<sup>th</sup> International Conference on Types for Proofs and Programs, TYPES 2020 ; Conference date: 02-05-2020 Through 05-05-2020",

url = "https://types2020.di.unito.it/",

}

From, AH 2021, Synthetic Completeness for a Terminating Seligman-Style Tableau System. in Proceedings of 26^th International Conference on Types for Proofs and Programs. Schloß Dagstuhl, Leibniz International Proceedings in Informatics, vol. 188, pp. 5:1--5:17, 26^th International Conference on Types for Proofs and Programs, Turin, Italy, 02/05/2020. https://doi.org/10.4230/LIPIcs.TYPES.2020.5

Synthetic Completeness for a Terminating Seligman-Style Tableau System. / From, Asta Halkjær.
Proceedings of 26^th International Conference on Types for Proofs and Programs. Schloß Dagstuhl, 2021. p. 5:1--5:17 (Leibniz International Proceedings in Informatics, Vol. 188).

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

TY - GEN

T1 - Synthetic Completeness for a Terminating Seligman-Style Tableau System

AU - From, Asta Halkjær

PY - 2021

Y1 - 2021

N2 - Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.

AB - Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.

KW - Hybrid logic

KW - Seligman-style tableau

KW - Synthetic completeness

KW - Isabelle/HOL

U2 - 10.4230/LIPIcs.TYPES.2020.5

DO - 10.4230/LIPIcs.TYPES.2020.5

M3 - Article in proceedings

SN - 978-3-95977-182-5

T3 - Leibniz International Proceedings in Informatics

SP - 5:1--5:17

BT - Proceedings of 26th International Conference on Types for Proofs and Programs

PB - Schloß Dagstuhl

T2 - 26<sup>th</sup> International Conference on Types for Proofs and Programs

Y2 - 2 May 2020 through 5 May 2020

ER -

Synthetic Completeness for a Terminating Seligman-Style Tableau System

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this