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 proceedingArticle in proceedingsResearchpeer-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 languageEnglish
Title of host publicationSelected Reflections in Language, Logic, and Information. ESSLLI 2019.
EditorsAlexandra Pavlova, Mina Young Pedersen, Raffaella Bernardi
PublisherSpringer
Publication date2024
Pages80-92
ISBN (Print)9783031506277
DOIs
Publication statusPublished - 2024
Event2019 European Summer School in Logic, Language and Information - University of Latvia, Riga, Latvia
Duration: 5 Aug 201916 Aug 2019

Conference

Conference2019 European Summer School in Logic, Language and Information
LocationUniversity of Latvia
Country/TerritoryLatvia
CityRiga
Period05/08/201916/08/2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14354 LNCS
ISSN0302-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

Cite this