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 language | English |
---|---|
Title of host publication | Intelligent Computer Mathematics |
Subtitle of host publication | 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings |
Publisher | Springer |
Pages | 38-52 |
Number of pages | 15 |
Volume | 5144 |
ISBN (Electronic) | 978-3-540-85110-3 |
ISBN (Print) | 978-3-540-85109-7 |
DOIs | |
Publication status | Published - 2008 |