Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

Asta Halkjær From; Agnes Moesgård  Eschen; Jørgen Villadsen

doi:10.1007/978-3-030-81097-9_3

Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

Asta Halkjær From
, Agnes Moesgård Eschen
, Jørgen Villadsen

Department of Applied Mathematics and Computer Science

Technical University of Denmark

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

329 Downloads (Orbit)

Abstract

We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

Original language	English
Title of host publication	Intelligent Computer Mathematics
Publisher	Springer
Publication date	2021
Pages	32-46
ISBN (Print)	978-3-030-81097-9
DOIs	https://doi.org/10.1007/978-3-030-81097-9_3
Publication status	Published - 2021
Event	14^th International Conference on Intelligent Computer Mathematics - Virtual event, Timisoara, Romania Duration: 26 Jul 2021 → 31 Jul 2021 https://cicm-conference.org/2021

Conference

Conference	14^th International Conference on Intelligent Computer Mathematics
Location	Virtual event
Country/Territory	Romania
City	Timisoara
Period	26/07/2021 → 31/07/2021
Internet address	https://cicm-conference.org/2021

Series	Lecture Notes in Computer Science
Volume	12833
ISSN	0302-9743

Keywords

Propositional Logic
Axiomatic Systems
Isabelle/HOL
Completeness
Soundness

Access to Document

10.1007/978-3-030-81097-9_3

FulltextAccepted author manuscript, 256 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{a8f3ad6ed47f450fa8895af864770732,

title = "Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL",

abstract = "We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL. ",

keywords = "Propositional Logic, Axiomatic Systems, Isabelle/HOL, Completeness, Soundness",

author = "From, \{Asta Halkj{\ae}r\} and Eschen, \{Agnes Moesg{\aa}rd\} and J{\o}rgen Villadsen",

year = "2021",

doi = "10.1007/978-3-030-81097-9\_3",

language = "English",

isbn = "978-3-030-81097-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "32--46",

booktitle = "Intelligent Computer Mathematics",

note = "14<sup>th</sup> International Conference on Intelligent Computer Mathematics, CICM 2021 ; Conference date: 26-07-2021 Through 31-07-2021",

url = "https://cicm-conference.org/2021",

}

TY - GEN

T1 - Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

AU - From, Asta Halkjær

AU - Eschen, Agnes Moesgård

AU - Villadsen, Jørgen

PY - 2021

Y1 - 2021

N2 - We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

AB - We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

KW - Propositional Logic

KW - Axiomatic Systems

KW - Isabelle/HOL

KW - Completeness

KW - Soundness

U2 - 10.1007/978-3-030-81097-9_3

DO - 10.1007/978-3-030-81097-9_3

M3 - Article in proceedings

SN - 978-3-030-81097-9

T3 - Lecture Notes in Computer Science

SP - 32

EP - 46

BT - Intelligent Computer Mathematics

PB - Springer

T2 - 14<sup>th</sup> International Conference on Intelligent Computer Mathematics

Y2 - 26 July 2021 through 31 July 2021

ER -

Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this