Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Propositional Proof Systems

view this post on Zulip Email Gateway (Aug 22 2022 at 15:38):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Propositional Proof Systems
by Julius Michaelis and Tobias Nipkow

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.

https://www.isa-afp.org/entries/Propositional_Proof_Systems.shtml

Enjoy,
René

Last updated: Apr 19 2024 at 20:15 UTC