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.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,881

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.

My notes

Similar books and articles

Predicate logics on display.Heinrich Wansing - 1999 - Studia Logica 62 (1):49-75.
Embedding display calculi into logical frameworks : Comparing twelf and Isabelle.Jeremy E. Dawson - unknown
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S.Rajeev Gore - manuscript
A Simple Proof of Completeness and Cut-elimination for Propositional G¨ odel Logic.Arnon Avron - unknown
Display calculi for logics with relative accessibility relations.Stéphane Demri & Rajeev Goré - 2000 - Journal of Logic, Language and Information 9 (2):213-236.
Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown

Analytics

Added to PP
2009-01-28

Downloads
174 (#111,833)

6 months
1 (#1,471,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