Mechanising cut-elimination for display logic
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|
|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.