Propositional Proof Systems

Julius Michaelis 🌐 and Tobias Nipkow 🌐

June 21, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Session Propositional_Proof_Systems