@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",
}