Deriving relational programs for computing kernels by reconstructing a proof of Richardsonʹs theorem

We combine relational algebra and program derivation methodology and reconstruct a proof of Richardsonʹs theorem that every finite directed graph without circuits of odd length has a kernel as a relational program. Also a generalization of the approach is presented.