Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL
Logic in Computer Science
2007-05-23 v1
Abstract
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.
Cite
@article{arxiv.cs/0607058,
title = {Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL},
author = {Tom Ridge},
journal= {arXiv preprint arXiv:cs/0607058},
year = {2007}
}