Mechanising cut-elimination for display logic
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]
Collections | ANU 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 | Size | Format | Image |
---|---|---|---|---|
TR-CS-01-02.pdf | 334.16 kB | Adobe PDF |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator