Formalized Proof Systems for Propositional Logic
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