Formalising Strong Normalisation for the Display Calculus of Relation Algebras in Isabelle/HOL

Rajeev Goré

Australian National University Canberra, Australia

Joint work with Jeremy E Dawson

Juin 14, 14h30, Salle du Conseil

Abstract: Relation algebras are important in computer science as the basis of relational databases. Display logic is a generalised sequent framework due to Nuel Belnap where any display calculus obeying certain easily checked conditions is guaranteed to obey cut-elimination. We describe a formalisation of a strong normalisation theorem for the display calculus of relation algebras using Isabelle/HOL. Since one proof fits all display calculi, this result is extremely general.

Back to schedule.

Marieke Huisman

Last modified: Tue Apr 3 2001