ANU Computer Science Technical Reports

TR-CS-01-02

Jeremy E. Dawson and Rajeev Gore.
Mechanising cut-elimination for display logic.
October 2001.

[POSTSCRIPT (161355 bytes)] [PDF (342177 bytes)] [EPrints archive]

Abstract: We describe a deep embedding of the display calculus \dRA, for relation algebras, using Isabelle/HOL. We then describe how the embedding was used to formalise a cut-elimination theorem for \dRA. 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 implementation in Isabelle/HOL.

Technical Reports <Technical-DOT-Reports-AT-cs-DOT-anu.edu.au>

Last modified: Tue May 31 12:56:00 EST 2011