Calculational Relation-Algebraic Proofs in Isabelle/Isar

Wolfram Kahl

pp. 178-190 in Rudolf Berghammer, Bernhard Möller, Georg Struth (ed.) Relational and {Kleene}-Algebraic Methods in Computer Science: {7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12--17, 2003, Revised Selected Papers, LNCS 3051, Springer-Verlag, 2003.



We propose a collection of theories in the proof assistant Isabelle/Isar that support calculational reasoning in and about heterogeneous relational algebras and Kleene algebras.

Wolfram Kahl