Skip navigation
Skip navigation

Mechanising cut-elimination for display logic

Dawson, Jeremy; Gore, Rajeev

Description

We describe a deep embedding of the display calculus ÆRA, for relation algebras, using Isabelle/HOL. We then describe how the embedding was used to formalise a cut-elimination theorem for ÆRA. Our implementation generalises easily to handle other display calculi. We consider a published proof of strong normalization of cut-elimination for Display Logic, and discuss the problems with it which prevented us from being able to implement it. We then give a different proof and describe its...[Show more]

CollectionsANU Research Publications
Date published: 2001
Type: Working/Technical Paper
URI: http://hdl.handle.net/1885/40728
http://digitalcollections.anu.edu.au/handle/1885/40728

Download

File Description SizeFormat Image
1546-01.2003-07-01T23:28:25Z.xsh356 BEPrints MD5 Hash XML
TR-CS-01-02.pdf334.16 kBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator