We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.
@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5, author = {Michaelis, Julius and Nipkow, Tobias}, title = {{Formalized Proof Systems for Propositional Logic}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5}, URN = {urn:nbn:de:0030-drops-100537}, doi = {10.4230/LIPIcs.TYPES.2017.5}, annote = {Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution} }
Feedback for Dagstuhl Publishing