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 proceedingArticle in proceedingsResearchpeer-review

44 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 202131 Jul 2021
https://cicm-conference.org/2021

Conference

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

Keywords

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

Cite this