Formalized Soundness and Completeness of Epistemic Logic

Asta Halkjær From

doi:10.1007/978-3-030-88853-4_1

Formalized Soundness and Completeness of Epistemic Logic

Asta Halkjær From

Department of Applied Mathematics and Computer Science

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

Abstract

We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.

Original language	English
Title of host publication	Logic, Language, Information, and Computation
Publisher	Springer
Publication date	2021
Pages	1-15
ISBN (Print)	978-3-030-88852-7
DOIs	https://doi.org/10.1007/978-3-030-88853-4_1
Publication status	Published - 2021
Event	27^th International Workshop on Logic, Language, Information and Computation - Online Event Duration: 5 Oct 2021 → 8 Oct 2021 Conference number: 27 https://link.springer.com/book/10.1007/978-3-030-88853-4

Workshop

Workshop	27^th International Workshop on Logic, Language, Information and Computation
Number	27
Location	Online Event
Period	05/10/2021 → 08/10/2021
Internet address	https://link.springer.com/book/10.1007/978-3-030-88853-4

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

Keywords

Canonicity
Completeness
Epistemic logic
Isabelle/HOL

Access to Document

10.1007/978-3-030-88853-4_1

OpenUrl availability

Full text

Cite this

@inbook{121abffe58314058b3a1776591a8c574,

title = "Formalized Soundness and Completeness of Epistemic Logic",

abstract = "We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.",

keywords = "Canonicity, Completeness, Epistemic logic, Isabelle/HOL",

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

year = "2021",

doi = "10.1007/978-3-030-88853-4\_1",

language = "English",

isbn = "978-3-030-88852-7",

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

publisher = "Springer",

pages = "1--15",

booktitle = "Logic, Language, Information, and Computation",

note = "27<sup>th</sup> International Workshop on Logic, Language, Information and Computation, WoLLIC 2021 ; Conference date: 05-10-2021 Through 08-10-2021",

url = "https://link.springer.com/book/10.1007/978-3-030-88853-4",

}

From, AH 2021, Formalized Soundness and Completeness of Epistemic Logic. in Logic, Language, Information, and Computation. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13038, pp. 1-15, 27^th International Workshop on Logic, Language, Information and Computation, 05/10/2021. https://doi.org/10.1007/978-3-030-88853-4_1

Formalized Soundness and Completeness of Epistemic Logic. / From, Asta Halkjær.
Logic, Language, Information, and Computation. Springer, 2021. p. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13038).

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

TY - CHAP

T1 - Formalized Soundness and Completeness of Epistemic Logic

AU - From, Asta Halkjær

N1 - Conference code: 27

PY - 2021

Y1 - 2021

N2 - We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.

AB - We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.

KW - Canonicity

KW - Completeness

KW - Epistemic logic

KW - Isabelle/HOL

U2 - 10.1007/978-3-030-88853-4_1

DO - 10.1007/978-3-030-88853-4_1

M3 - Book chapter

SN - 978-3-030-88852-7

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

SP - 1

EP - 15

BT - Logic, Language, Information, and Computation

PB - Springer

T2 - 27<sup>th</sup> International Workshop on Logic, Language, Information and Computation

Y2 - 5 October 2021 through 8 October 2021

ER -

Formalized Soundness and Completeness of Epistemic Logic

Abstract

Workshop

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this