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

1 Citation (Scopus)

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. CICM 2008
PublisherSpringer
Pages38-52
Number of pages15
ISBN (Electronic)9783540851103
ISBN (Print)3540851097, 9783540851097
DOIs
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
Volume5144
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Automated reasoning
  • Formal mathematics
  • Logic
  • Nominal Isabelle

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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