Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)

Asta Halkjær From; Patrick Rowan Blackburn; Jørgen Villadsen

doi:10.1007/978-3-030-51074-9_27

Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)

Asta Halkjær From^*, Patrick Rowan Blackburn, Jørgen Villadsen

^*Corresponding author for this work

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

Abstract

Hybrid logic is modal logic enriched with names for worlds.We formalize soundness and completeness proofs for a Seligman-styletableau system for hybrid logic in the proof assistant Isabelle/HOL. Theformalization shows how to lift certain rule restrictions, thereby simpli-fying the original un-formalized proof. Moreover, the completeness proofwe formalize is synthetic which suggests we can extend this work to provea wider range of results about hybrid logic.

Original language	English
Title of host publication	Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
Editors	Nicolas Peltier, Viorica Sofronie-Stokkermans
Number of pages	8
Publisher	Springer
Publication date	2020
Pages	474-481
ISBN (Print)	9783030510732
DOIs	https://doi.org/10.1007/978-3-030-51074-9_27
Publication status	Published - 2020
Event	International Joint Conference on Automated Reasoning 2020 - Le Centre de Colloques, Paris, France Duration: 29 Jun 2020 → 6 Jul 2020 https://ijcar2020.org/

Conference

Conference	International Joint Conference on Automated Reasoning 2020
Location	Le Centre de Colloques
Country/Territory	France
City	Paris
Period	29/06/2020 → 06/07/2020
Internet address	https://ijcar2020.org/

Keywords

Completness
Hybrid logic
Isabell/HOL
Proof assistant
Seligman-style
Soundness
Tableaus

Link to document

10.1007/978-3-030-51074-9_27

Cite this

Halkjær From, A., Blackburn, P. R., & Villadsen, J. (2020). Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper). In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I (pp. 474-481). Springer. https://doi.org/10.1007/978-3-030-51074-9_27

@inproceedings{2ad011dbfbbf4b988218b61e5b7af549,

title = "Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)",

abstract = "Hybrid logic is modal logic enriched with names for worlds.We formalize soundness and completeness proofs for a Seligman-styletableau system for hybrid logic in the proof assistant Isabelle/HOL. Theformalization shows how to lift certain rule restrictions, thereby simpli-fying the original un-formalized proof. Moreover, the completeness proofwe formalize is synthetic which suggests we can extend this work to provea wider range of results about hybrid logic.",

keywords = "Completness, Hybrid logic, Isabell/HOL, Proof assistant, Seligman-style, Soundness, Tableaus, Completness, Hybrid logic, Isabelle/HOL, Proff assistant, Seligman-style, Soundness, Tableaus",

author = "{Halkj{\ae}r From}, Asta and Blackburn, {Patrick Rowan} and J{\o}rgen Villadsen",

year = "2020",

doi = "10.1007/978-3-030-51074-9_27",

language = "English",

isbn = "9783030510732",

pages = "474--481",

editor = "Nicolas Peltier and Viorica Sofronie-Stokkermans",

booktitle = "Automated Reasoning",

publisher = "Springer",

note = "International Joint Conference on Automated Reasoning 2020, IJCAR 2020 ; Conference date: 29-06-2020 Through 06-07-2020",

url = "https://ijcar2020.org/",

}

Halkjær From, A, Blackburn, PR & Villadsen, J 2020, Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper). in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. Springer, pp. 474-481, International Joint Conference on Automated Reasoning 2020, Paris, France, 29/06/2020. https://doi.org/10.1007/978-3-030-51074-9_27

Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper). / Halkjær From, Asta; Blackburn, Patrick Rowan; Villadsen, Jørgen.
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. ed. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Springer, 2020. p. 474-481.

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

TY - GEN

T1 - Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)

AU - Halkjær From, Asta

AU - Blackburn, Patrick Rowan

AU - Villadsen, Jørgen

PY - 2020

Y1 - 2020

N2 - Hybrid logic is modal logic enriched with names for worlds.We formalize soundness and completeness proofs for a Seligman-styletableau system for hybrid logic in the proof assistant Isabelle/HOL. Theformalization shows how to lift certain rule restrictions, thereby simpli-fying the original un-formalized proof. Moreover, the completeness proofwe formalize is synthetic which suggests we can extend this work to provea wider range of results about hybrid logic.

AB - Hybrid logic is modal logic enriched with names for worlds.We formalize soundness and completeness proofs for a Seligman-styletableau system for hybrid logic in the proof assistant Isabelle/HOL. Theformalization shows how to lift certain rule restrictions, thereby simpli-fying the original un-formalized proof. Moreover, the completeness proofwe formalize is synthetic which suggests we can extend this work to provea wider range of results about hybrid logic.

KW - Completness

KW - Hybrid logic

KW - Isabell/HOL

KW - Proof assistant

KW - Seligman-style

KW - Soundness

KW - Tableaus

KW - Completness

KW - Hybrid logic

KW - Isabelle/HOL

KW - Proff assistant

KW - Seligman-style

KW - Soundness

KW - Tableaus

UR - https://link.springer.com/chapter/10.1007/978-3-030-51074-9_27

U2 - 10.1007/978-3-030-51074-9_27

DO - 10.1007/978-3-030-51074-9_27

M3 - Article in proceedings

SN - 9783030510732

SP - 474

EP - 481

BT - Automated Reasoning

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - Springer

T2 - International Joint Conference on Automated Reasoning 2020

Y2 - 29 June 2020 through 6 July 2020

ER -

Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)

Abstract

Conference

Keywords

Link to document

Other files and links

Cite this