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

Peter Chapman, James McKinna, Christian Urban

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings
PublisherSpringer
Pages38-52
Number of pages15
Volume5144
ISBN (Electronic)978-3-540-85110-3
ISBN (Print)978-3-540-85109-7
DOIs
Publication statusPublished - 2008

Fingerprint

Dive into the research topics of 'Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle'. Together they form a unique fingerprint.

Cite this