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

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
Redaktører	Nicolas Peltier, Viorica Sofronie-Stokkermans
Antal sider	8
Forlag	Springer
Publikationsdato	2020
Sider	474-481
ISBN (Trykt)	9783030510732
DOI	https://doi.org/10.1007/978-3-030-51074-9_27
Status	Udgivet - 2020
Begivenhed	International Joint Conference on Automated Reasoning 2020 - Le Centre de Colloques, Paris, Frankrig Varighed: 29 jun. 2020 → 6 jul. 2020 https://ijcar2020.org/

Konference

Konference	International Joint Conference on Automated Reasoning 2020
Lokation	Le Centre de Colloques
Land/Område	Frankrig
By	Paris
Periode	29/06/2020 → 06/07/2020
Internetadresse	https://ijcar2020.org/

Emneord

Completness
Hybrid logic
Isabelle/HOL
Proff assistant
Seligman-style
Soundness
Tableaus

Link til dokument

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

Andre filer og links

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

Citer dette

Halkjær From, A., Blackburn, P. R., & Villadsen, J. (2020). Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper). I N. Peltier, & V. Sofronie-Stokkermans (red.), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I (s. 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). i N Peltier & V Sofronie-Stokkermans (red), Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. Springer, s. 474-481, International Joint Conference on Automated Reasoning 2020, Paris, Frankrig, 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. red. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Springer, 2020. s. 474-481.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › 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 -