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. (2019). Formalized Proof Systems for Propositional Logic (Version 1.0). Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik.

Session Propositional_Proof_Systems