Propositional Proof Systems

Julius Michaelis 🌐 and Tobias Nipkow 🌐

June 21, 2017


We formalize a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) and prove the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.


BSD License


Related publications

  • Michaelis, J., & Nipkow, T. (2018). Formalized Proof Systems for Propositional Logic. Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik GmbH, Wadern/Saarbruecken, Germany.

Session Propositional_Proof_Systems