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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

31 Downloads (Pure)

Abstract

We formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. Our formalization precisely details the structure of this proof method.
Original languageEnglish
Title of host publicationProceedings of the ESSLLI & WeSSLLI Student Session 2020
Publication date2020
Pages1-12
Publication statusPublished - 2020
EventWeb Summer School in Logic, Language, and Information
- Virtual event
Duration: 11 Jul 202017 Jul 2020
https://www.brandeis.edu/nasslli2020/index.html

Workshop

WorkshopWeb Summer School in Logic, Language, and Information
LocationVirtual event
Period11/07/202017/07/2020
Internet address

Keywords

  • Propositional logic
  • Henkin-style completeness
  • Isabelle/HOL

Cite this