Formalised cut admissibility for display logic

Jeremy E. Dawson

doi:10.1007/3-540-45685-6_10

Formalised cut admissibility for display logic

Jeremy E. Dawson

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

13 Citations (Scopus)

Abstract

We use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for δRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/ HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings
Editors	Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar
Publisher	Springer Verlag
Pages	131-147
Number of pages	17
ISBN (Print)	3540440399
DOIs	https://doi.org/10.1007/3-540-45685-6_10
Publication status	Published - 2002
Event	15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002 - Hampton, United States Duration: 20 Aug 2002 → 23 Aug 2002

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2410
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002
Country/Territory	United States
City	Hampton
Period	20/08/02 → 23/08/02

Access to Document

10.1007/3-540-45685-6_10

Cite this

Dawson, J. E. (2002). Formalised cut admissibility for display logic. In V. A. Carreno, C. A. Munoz, & S. Tahar (Eds.), Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings (pp. 131-147). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2410). Springer Verlag. https://doi.org/10.1007/3-540-45685-6_10

Dawson, Jeremy E. / Formalised cut admissibility for display logic. Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings. editor / Victor A. Carreno ; Cesar A. Munoz ; Sofiene Tahar. Springer Verlag, 2002. pp. 131-147 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{39e54b372cba440b9a0e0827c0822230,

title = "Formalised cut admissibility for display logic",

abstract = "We use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for δRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/ HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.",

author = "Dawson, {Jeremy E.}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002 ; Conference date: 20-08-2002 Through 23-08-2002",

year = "2002",

doi = "10.1007/3-540-45685-6_10",

language = "English",

isbn = "3540440399",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "131--147",

editor = "Carreno, {Victor A.} and Munoz, {Cesar A.} and Sofiene Tahar",

booktitle = "Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings",

address = "Germany",

}

Dawson, JE 2002, Formalised cut admissibility for display logic. in VA Carreno, CA Munoz & S Tahar (eds), Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2410, Springer Verlag, pp. 131-147, 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, Hampton, United States, 20/08/02. https://doi.org/10.1007/3-540-45685-6_10

Formalised cut admissibility for display logic. / Dawson, Jeremy E.
Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings. ed. / Victor A. Carreno; Cesar A. Munoz; Sofiene Tahar. Springer Verlag, 2002. p. 131-147 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2410).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formalised cut admissibility for display logic

AU - Dawson, Jeremy E.

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2002.

PY - 2002

Y1 - 2002

N2 - We use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for δRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/ HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

AB - We use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for δRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/ HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

UR - http://www.scopus.com/inward/record.url?scp=84919952655&partnerID=8YFLogxK

U2 - 10.1007/3-540-45685-6_10

DO - 10.1007/3-540-45685-6_10

M3 - Conference contribution

SN - 3540440399

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 131

EP - 147

BT - Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings

A2 - Carreno, Victor A.

A2 - Munoz, Cesar A.

A2 - Tahar, Sofiene

PB - Springer Verlag

T2 - 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002

Y2 - 20 August 2002 through 23 August 2002

ER -

Dawson JE. Formalised cut admissibility for display logic. In Carreno VA, Munoz CA, Tahar S, editors, Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Proceedings. Springer Verlag. 2002. p. 131-147. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45685-6_10

Formalised cut admissibility for display logic

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this