@inproceedings{c8b6f715b2e84239bc81de1667815110,

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 = "Formal mathematics, nominal Isabelle, automated reasoning, logic",

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

year = "2008",

month = jan,

day = "1",

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

language = "English",

isbn = "9783540851097",

volume = "5144",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "38--52",

booktitle = "Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics",

note = "Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics ; Conference date: 01-01-2008",

}