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. (2018). Formalized Proof Systems for Propositional Logic. Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik GmbH, Wadern/Saarbruecken, Germany. https://doi.org/10.4230/LIPICS.TYPES.2017.5

Session Propositional_Proof_Systems

Used by

Cite

× 
@article{Propositional_Proof_Systems-AFP,
  author  = {Julius Michaelis and Tobias Nipkow},
  title   = {Propositional Proof Systems},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/Propositional_Proof_Systems.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: