Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic

Asta Halkjær From

doi:10.1007/978-3-031-50628-4_5

Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic

Asta Halkjær From^*

^*Corresponding author for this work

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

Abstract

I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.

Original language	English
Title of host publication	Selected Reflections in Language, Logic, and Information. ESSLLI 2019.
Editors	Alexandra Pavlova, Mina Young Pedersen, Raffaella Bernardi
Publisher	Springer
Publication date	2024
Pages	80-92
ISBN (Print)	9783031506277
DOIs	https://doi.org/10.1007/978-3-031-50628-4_5
Publication status	Published - 2024
Event	2019 European Summer School in Logic, Language and Information - University of Latvia, Riga, Latvia Duration: 5 Aug 2019 → 16 Aug 2019

Conference

Conference	2019 European Summer School in Logic, Language and Information
Location	University of Latvia
Country/Territory	Latvia
City	Riga
Period	05/08/2019 → 16/08/2019

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

Bibliographical note

Publisher Copyright:
© 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Keywords

Henkin-style completeness
Isabelle/HOL
Propositional logic

Access to Document

10.1007/978-3-031-50628-4_5

OpenUrl availability

Full text

Cite this

From, Asta Halkjær. / Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic. Selected Reflections in Language, Logic, and Information. ESSLLI 2019. . editor / Alexandra Pavlova ; Mina Young Pedersen ; Raffaella Bernardi. Springer, 2024. pp. 80-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14354 LNCS).

@inproceedings{8f99484d9e6d4da09803fdac811394e8,

title = "Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic",

abstract = "I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.",

keywords = "Henkin-style completeness, Isabelle/HOL, Propositional logic",

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

note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 2019 European Summer School in Logic, Language and Information, ESSLLI 2019 ; Conference date: 05-08-2019 Through 16-08-2019",

year = "2024",

doi = "10.1007/978-3-031-50628-4_5",

language = "English",

isbn = "9783031506277",

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

publisher = "Springer",

pages = "80--92",

editor = "Alexandra Pavlova and Pedersen, {Mina Young} and Raffaella Bernardi",

booktitle = "Selected Reflections in Language, Logic, and Information. ESSLLI 2019.",

}

From, AH 2024, Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic. in A Pavlova, MY Pedersen & R Bernardi (eds), Selected Reflections in Language, Logic, and Information. ESSLLI 2019. . Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14354 LNCS, pp. 80-92, 2019 European Summer School in Logic, Language and Information, Riga, Latvia, 05/08/2019. https://doi.org/10.1007/978-3-031-50628-4_5

Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic. / From, Asta Halkjær.
Selected Reflections in Language, Logic, and Information. ESSLLI 2019. . ed. / Alexandra Pavlova; Mina Young Pedersen; Raffaella Bernardi. Springer, 2024. p. 80-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14354 LNCS).

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

TY - GEN

T1 - Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic

AU - From, Asta Halkjær

PY - 2024

Y1 - 2024

N2 - I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.

AB - I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.

KW - Henkin-style completeness

KW - Isabelle/HOL

KW - Propositional logic

U2 - 10.1007/978-3-031-50628-4_5

DO - 10.1007/978-3-031-50628-4_5

M3 - Article in proceedings

AN - SCOPUS:85181981097

SN - 9783031506277

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

SP - 80

EP - 92

BT - Selected Reflections in Language, Logic, and Information. ESSLLI 2019.

A2 - Pavlova, Alexandra

A2 - Pedersen, Mina Young

A2 - Bernardi, Raffaella

PB - Springer

T2 - 2019 European Summer School in Logic, Language and Information

Y2 - 5 August 2019 through 16 August 2019

ER -

From AH. Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic. In Pavlova A, Pedersen MY, Bernardi R, editors, Selected Reflections in Language, Logic, and Information. ESSLLI 2019. . Springer. 2024. p. 80-92. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14354 LNCS). doi: 10.1007/978-3-031-50628-4_5