zbMATH — the first resource for mathematics

A new machine-checked proof of strong normalisation for display logic. (English) Zbl 1270.03119
Harland, James (ed.), CATS’03. Computing: the Australasian theory symposium. Proceedings of the symposium, Monash, Australia, February 4–7, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 78, 20-39 (2003).
Summary: We use a deep embedding of the display calculus for relation algebras \(\delta\mathsf{RA}\) in the logical framework Isabelle/HOL to formalise a new, machine-checked, proof of strong normalisation and cut elimination for \(\delta\mathsf{RA}\) which does not use measures on the size of derivations. Our formalisation generalises easily to other display calculi and can serve as a basis for formalised proofs of strong normalisation for the classical and intuitionistic versions of a vast range of substructural logics like the Lambek calculus, linear logic, relevant logic, BCK-logic, and their modal extensions. We believe this is the first full formalisation of a strong normalisation result for a sequent system using a logical framework.
For the entire collection see [Zbl 1270.68028].

03F05 Cut-elimination and normal-form theorems
03B35 Mechanization of proofs and logical operations
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: Link