@inproceedings{fa46265029ea45eeb9fb72ab2c5610b1,

title = "Mechanising a proof of Craig's interpolation theorem for intuitionistic logic in nominal Isabelle",

abstract = "Craig's Interpolation Theorem is an important meta- theoretical result for several logics. Here we describe a formalisation of the result for first-order intuitionistic logic without function symbols or equality, with the intention of giving insight into how other such results in proof theory might be mechanically verified, notable cut-admissibility. We use the package Nominal Isabelle, which easily deals with the binding issues in the quantifier cases of the proof.",

keywords = "Automated reasoning, Formal mathematics, Logic, Nominal Isabelle",

author = "Peter Chapman and James McKinna and Christian Urban",

year = "2008",

doi = "10.1007/978-3-540-85110-3_5",

language = "English",

isbn = "3540851097",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "38--52",

booktitle = "Intelligent Computer Mathematics. CICM 2008",

}