Formalized Proof Systems for Propositional Logic

Julius Michaelis and Tobias Nipkow

We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most impor- tant meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.

pdf

BibTeX:

@inproceedings{MichaelisN-TYPES17,
  author    = {Julius Michaelis and Tobias Nipkow},
  title     = {Formalized Proof Systems for Propositional Logic},
  booktitle = {23rd Int.\ Conf.\ Types for Proofs and Programs (TYPES 2017)},
  editor    = {A. Abel and F. Nordvall Forsberg and A. Kaposi},
  series    = {LIPIcs},
  volume    = {104},
  pages     = {6:1--6:16},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2018}
}

DOI

Isabelle theories in the Archive of Formal Proofs