# Propositional Proof Systems

 Title: Propositional Proof Systems Authors: Julius Michaelis and Tobias Nipkow Submission date: 2017-06-21 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. BibTeX: @article{Propositional_Proof_Systems-AFP, author = {Julius Michaelis and Tobias Nipkow}, title = {Propositional Proof Systems}, journal = {Archive of Formal Proofs}, month = jun, year = 2017, note = {\url{https://isa-afp.org/entries/Propositional_Proof_Systems.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: AI_Planning_Languages_Semantics, Verified_SAT_Based_AI_Planning