Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)

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

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

Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)

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

^*Corresponding author for this work

Department of Applied Mathematics and Computer Science

Roskilde University

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-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.

Original language	English
Title of host publication	Proceedings of 10^th International Joint Conference Automated Reasoning
Editors	Nicolas Peltier, Viorica Sofronie-Stokkermans
Publisher	Springer
Publication date	1 Jan 2020
Pages	474-481
ISBN (Print)	9783030510732
DOIs	https://doi.org/10.1007/978-3-030-51074-9_27
Publication status	Published - 1 Jan 2020
Event	10th International Joint Conference on Automated Reasoning - Virtual, Online Duration: 29 Jun 2020 → 5 Jul 2020 Conference number: 10

Conference

Conference	10th International Joint Conference on Automated Reasoning
Number	10
City	Virtual, Online
Period	29/06/2020 → 05/07/2020

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12166 LNAI
ISSN	0302-9743

Keywords

Completeness
Hybrid logic
Isabelle/HOL
Soundness

Access to Document

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

OpenUrl availability

Full text

Cite this

From, Asta Halkjær ; Blackburn, Patrick ; Villadsen, Jørgen. / Formalizing a Seligman-Style Tableau System for Hybrid Logic : (Short Paper). Proceedings of 10^th International Joint Conference Automated Reasoning. editor / Nicolas Peltier ; Viorica Sofronie-Stokkermans. Springer, 2020. pp. 474-481 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12166 LNAI).

@inproceedings{ee3b0b62f5ab492cb8da88b813124d86,

title = "Formalizing a Seligman-Style Tableau System 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-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.",

keywords = "Completeness, Hybrid logic, Isabelle/HOL, Soundness",

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

year = "2020",

month = jan,

day = "1",

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

language = "English",

isbn = "9783030510732",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "474--481",

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

booktitle = "Proceedings of 10th International Joint Conference Automated Reasoning",

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

}

From, AH, Blackburn, P & Villadsen, J 2020, Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper). in N Peltier & V Sofronie-Stokkermans (eds), Proceedings of 10^th International Joint Conference Automated Reasoning. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12166 LNAI, pp. 474-481, 10th International Joint Conference on Automated Reasoning, Virtual, Online, 29/06/2020. https://doi.org/10.1007/978-3-030-51074-9_27

Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper). / From, Asta Halkjær; Blackburn, Patrick; Villadsen, Jørgen.
Proceedings of 10^th International Joint Conference Automated Reasoning. ed. / Nicolas Peltier; Viorica Sofronie-Stokkermans. Springer, 2020. p. 474-481 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12166 LNAI).

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

TY - GEN

T1 - Formalizing a Seligman-Style Tableau System for Hybrid Logic

T2 - 10th International Joint Conference on Automated Reasoning

AU - From, Asta Halkjær

AU - Blackburn, Patrick

AU - Villadsen, Jørgen

N1 - Conference code: 10

PY - 2020/1/1

Y1 - 2020/1/1

N2 - Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a 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-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.

KW - Completeness

KW - Hybrid logic

KW - Isabelle/HOL

KW - Soundness

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

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

M3 - Article in proceedings

AN - SCOPUS:85088237743

SN - 9783030510732

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

SP - 474

EP - 481

BT - Proceedings of 10th International Joint Conference Automated Reasoning

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - Springer

Y2 - 29 June 2020 through 5 July 2020

ER -

From AH, Blackburn P, Villadsen J. Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper). In Peltier N, Sofronie-Stokkermans V, editors, Proceedings of 10^th International Joint Conference Automated Reasoning. Springer. 2020. p. 474-481. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 12166 LNAI). doi: 10.1007/978-3-030-51074-9_27

Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this