Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

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

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

187 Downloads (Pure)

Abstract

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

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
PublisherSpringer
Publication date2021
Pages32-46
ISBN (Print)978-3-030-81097-9
DOIs
Publication statusPublished - 2021
Event14th International Conference on Intelligent Computer Mathematics - Virtual event, Timisoara, Romania
Duration: 26 Jul 2021 → 31 Jul 2021
https://cicm-conference.org/2021

Conference

Conference14th International Conference on Intelligent Computer Mathematics
LocationVirtual event
Country/TerritoryRomania
CityTimisoara
Period26/07/2021 → 31/07/2021
Internet address
SeriesLecture Notes in Computer Science
Volume12833
ISSN0302-9743

Keywords

  • Propositional Logic
  • Axiomatic Systems
  • Isabelle/HOL
  • Completeness
  • Soundness

Access to Document

  • FulltextAccepted author manuscript, 256 KB

OpenUrl availability

Full text

    Fingerprint

    Dive into the research topics of 'Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL'. Together they form a unique fingerprint.
    View full fingerprint

    Cite this