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/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBNpeer-review

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 publicationProceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics
Place of PublicationBerlin Heidelberg, Germany
PublisherSpringer Berlin Heidelberg
Pages38-52
Number of pages15
Volume5144
ISBN (Print)9783540851097
DOIs
Publication statusPublished - 1 Jan 2008
EventProceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics - Birmingham, UK, July 28 - August 1, 2008
Duration: 1 Jan 2008 → …

Publication series

NameLecture Notes in Computer Science

Conference

ConferenceProceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics
Period1/01/08 → …

Keywords

  • Formal mathematics
  • nominal Isabelle
  • automated reasoning
  • logic

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