Abstract
Binary relations are one of the standard ways to encode, characterise
and reason about graphs. Relation algebras provide equational axioms
for a large fragment of the calculus of binary relations. Although
relations are standard tools in many areas of mathematics and
computing, researchers usually fall back to point-wise reasoning when
it comes to arguments about paths in a graph. We present a purely
algebraic way to specify different kinds of paths in Kleene relation
algebras, which are relation algebras equipped with an operation for
reflexive transitive closure. We study the relationship between paths
with a designated root vertex and paths without such a vertex. Since
we stay in first-order logic this development helps with mechanising
proofs. To demonstrate the applicability of the algebraic framework we
verify the correctness of three basic graph algorithms.