references.bib

@misc{guo_verified_2023,
  title      = {Verified completeness in Henkin-style for intuitionistic propositional logic},
  url        = {http://arxiv.org/abs/2310.01916},
  abstract   = {This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen’s method in the literature. The full source code can be found online at https://github.com/bbentzen/ipl.},
  number     = {{arXiv}:2310.01916},
  publisher  = {{arXiv}},
  author     = {Guo, Huayu and Chen, Dongheng and Bentzen, Bruno},
  urldate    = {2024-07-04},
  date       = {2023-10-03},
  langid     = {english},
  eprinttype = {arxiv},
  eprint     = {2310.01916 [cs]},
  keywords   = {Computer Science - Logic in Computer Science},
  file       = {Guo et al. - 2023 - Verified completeness in Henkin-style for intuitio.pdf:C\:\\Users\\SnO2WMaN\\Zotero\\storage\\ZFNM8CZJ\\Guo et al. - 2023 - Verified completeness in Henkin-style for intuitio.pdf:application/pdf}
}

@incollection{bentzen_henkin-style_2021,
  title      = {A Henkin-style completeness proof for the modal logic S5},
  volume     = {13040},
  url        = {http://arxiv.org/abs/1910.01697},
  abstract   = {This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover [5]. The proof formalized is close to that of Hughes and Cresswell [11], but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical connectives and necessity as the only primitive modal operator. The full source code is available online at https://github.com/bbentzen/mpl/ and has been typechecked with Lean 3.4.2.},
  pages      = {459--467},
  author     = {Bentzen, Bruno},
  urldate    = {2024-07-04},
  date       = {2021},
  langid     = {english},
  doi        = {10.1007/978-3-030-89391-0_25},
  eprinttype = {arxiv},
  eprint     = {1910.01697 [cs]},
  keywords   = {Computer Science - Logic in Computer Science},
  file       = {Bentzen - 2021 - A Henkin-style completeness proof for the modal lo.pdf:C\:\\Users\\SnO2WMaN\\Zotero\\storage\\UPI9UBEN\\Bentzen - 2021 - A Henkin-style completeness proof for the modal lo.pdf:application/pdf}
}