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.

Abstract

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.

License

BSD License

Topics

Related publications

  • Michaelis, J., & Nipkow, T. (2019). Formalized Proof Systems for Propositional Logic (Version 1.0). Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik. https://doi.org/10.4230/LIPICS.TYPES.2017.5

Session Propositional_Proof_Systems