Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

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.

• Type: Conference
• Year: 2008
• Where: AISC
• Authors: Peter Chapman, James McKinna, Christian Urban
• Keywords: AISC 2008, Artificial Intelligence, Craig's Interpolation Theorem, First-order Intuitionistic Logic, Package Nominal Isabelle