Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle

Peter Chapman; James McKinna; Christian Urban

doi:10.1007/978-3-540-85110-3_5

Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle

Peter Chapman, James McKinna, Christian Urban

University of Brighton

Research output: Chapter in Book/Conference proceeding with ISSN or ISBN › Conference contribution with ISSN or ISBN › peer-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 language	English
Title of host publication	Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics
Place of Publication	Berlin Heidelberg, Germany
Publisher	Springer Berlin Heidelberg
Pages	38-52
Number of pages	15
Volume	5144
ISBN (Print)	9783540851097
DOIs	https://doi.org/10.1007/978-3-540-85110-3_5
Publication status	Published - 1 Jan 2008
Event	Proceedings 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

Name	Lecture Notes in Computer Science

Conference

Conference	Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics
Period	1/01/08 → …

Keywords

Formal mathematics
nominal Isabelle
automated reasoning
logic

Access to Document

10.1007/978-3-540-85110-3_5Licence: Unspecified

http://dl.acm.org/citation.cfm?id=1428596Licence: Unspecified

Cite this

Chapman, P., McKinna, J., & Urban, C. (2008). Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle. In Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics (Vol. 5144, pp. 38-52). (Lecture Notes in Computer Science). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_5

Chapman, Peter ; McKinna, James ; Urban, Christian. / Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle. Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics. Vol. 5144 Berlin Heidelberg, Germany : Springer Berlin Heidelberg, 2008. pp. 38-52 (Lecture Notes in Computer Science).

@inproceedings{c8b6f715b2e84239bc81de1667815110,

title = "Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle",

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.",

keywords = "Formal mathematics, nominal Isabelle, automated reasoning, logic",

author = "Peter Chapman and James McKinna and Christian Urban",

year = "2008",

month = jan,

day = "1",

doi = "10.1007/978-3-540-85110-3_5",

language = "English",

isbn = "9783540851097",

volume = "5144",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "38--52",

booktitle = "Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics",

note = "Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics ; Conference date: 01-01-2008",

}

Chapman, P, McKinna, J & Urban, C 2008, Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle. in Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics. vol. 5144, Lecture Notes in Computer Science, Springer Berlin Heidelberg, Berlin Heidelberg, Germany, pp. 38-52, Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics, 1/01/08. https://doi.org/10.1007/978-3-540-85110-3_5

Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle. / Chapman, Peter; McKinna, James; Urban, Christian.
Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics. Vol. 5144 Berlin Heidelberg, Germany: Springer Berlin Heidelberg, 2008. p. 38-52 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Conference proceeding with ISSN or ISBN › Conference contribution with ISSN or ISBN › peer-review

TY - GEN

T1 - Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle

AU - Chapman, Peter

AU - McKinna, James

AU - Urban, Christian

PY - 2008/1/1

Y1 - 2008/1/1

N2 - 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.

AB - 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.

KW - Formal mathematics

KW - nominal Isabelle

KW - automated reasoning

KW - logic

U2 - 10.1007/978-3-540-85110-3_5

DO - 10.1007/978-3-540-85110-3_5

M3 - Conference contribution with ISSN or ISBN

SN - 9783540851097

VL - 5144

T3 - Lecture Notes in Computer Science

SP - 38

EP - 52

BT - Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics

PB - Springer Berlin Heidelberg

CY - Berlin Heidelberg, Germany

T2 - Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics

Y2 - 1 January 2008

ER -

Chapman P, McKinna J, Urban C. Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle. In Proceedings of the 9th AISC international conference, the 15th Calculemas symposium, and the 7th international MKM conference on Intelligent Computer Mathematics. Vol. 5144. Berlin Heidelberg, Germany: Springer Berlin Heidelberg. 2008. p. 38-52. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-85110-3_5

Mechanising a proof of Craig's Interpolation Theorem for intuitionistic logic in nominal isabelle

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this