Formalized Proof Systems for Propositional Logic
Michaelis, Julius, Nipkow, Tobias · arXiv (Cornell University) · 2019
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 important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.