2019/01/01 by Rodolphe Lepigre, Michaelis, Julius, Nipkow, Tobias · 7 citations
Computer Science · Mathematics · #Algebra over a field #Automated theorem proving #Calculus (dental) #Computer science #Dependent type #Formal Methods in Verification #Function (biology) #Lambda calculus #Logic, programming, and type systems #Mathematical proof #Mathematics #Operator (biology) #Parallel Computing and Optimization Techniques #Programming language #Pure mathematics #Recursion (computer science) #Subtyping #Theoretical computer science #Type (biology) #Type theory #cs.LO #cs.PL
paper · pdf · open access · doi:10.4230/lipics.types.2017.5
published in DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) (Schloss Dagstuhl – Leibniz Center for Informatics)
openalex publication_date 2019/01/01 · arxiv created 2019/01/10 · arxiv updated 2019/01/11 · openalex created_date 2019/01/25 · openalex updated_date 2026/08/05
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.