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,386

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

Formalised cut admissibility for display logic.Rajeev Gore - manuscript
Embedding display calculi into logical frameworks : Comparing twelf and Isabelle.Jeremy E. Dawson - unknown
Analytic cut trees.Carlo Cellucci - 2000 - Logic Journal of the IGPL 8 (6):733-750.
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Preventive War 'the Supreme Crime'.Noam Chomsky - unknown
How Bad Is Rape?H. E. Baber - 1987 - Hypatia 2 (2):125-138.
Preaching on the Environment.Holmes Rolston - unknown
The Hiddenness Argument Revisited.J. L. Schellenberg - 2005 - Religious Studies 41 (3):287-303.
A Novel Interpretation of Plato’s Theory of Forms.P. X. Monaghan - 2010 - Metaphysica 11 (1):63-78.
Correspondence, Invariance and Heuristics: Essays in Honour of Heinz Post.S. French & H. Kamminga (eds.) - 1993 - Dordrecht: Reidel.
Commodification or Compensation: A Reply to Ketchum.H. M. Malm - 1989 - Hypatia 4 (3):128-135.
Shifting Frames: From Divided to Distributed Psychologies of Scientific Agents.Peter J. Taylor - 1994 - PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1994:304-310.
The Contemporary Significance of Confucianism.Tang Yijie & Yan Xin - 2008 - Frontiers of Philosophy in China 3 (4):477-501.
The Aggressiveness of Playful Arguments.Dale Hample, Bing Han & David Payne - 2010 - Argumentation 24 (4):405-421.

Analytics

Added to PP
2010-12-22

Downloads
4 (#1,595,600)

6 months
2 (#1,232,442)

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

No references found.

Add more references