Sciweavers

AISC
2008
Springer

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

13 years 5 months ago
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.
Peter Chapman, James McKinna, Christian Urban
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AISC
Authors Peter Chapman, James McKinna, Christian Urban
Comments (0)