Programming and automating mathematics in the Tarski-Kleene hierarchy

We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how mo ...