Skip navigation
Skip navigation

Mechanising cut-elimination for display logic

Dawson, Jeremy; Gore, Rajeev


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


File Description SizeFormat Image
TR-CS-01-02.pdf334.16 kBAdobe PDFThumbnail

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

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator