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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 89,703

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Analytics

Added to PP
2009-01-28

Downloads
174 (#101,231)

6 months
1 (#1,017,540)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Display logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Substructural logics on display.R. Goré - 1998 - Logic Journal of the IGPL 6 (3):451-504.

Add more references