2006/07/12 by Tom Ridge, Ridge, Tom
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0607058
arxiv created 2006/07/12 · openalex publication_date 2006/07/12 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We formalise and mechanise a construtive, proof theoretic proof of Craig's Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma statements both formally and informally. We also transcribe informally the formal proofs. We detail the main features of our mechanisation, such as the formalisation of binding for first order formulae. We also give some applications of Craig's Interpolation Theorem.