From: Tobias Nipkow <nipkow@in.tum.de>

Relational Characterisations of Paths

Walter Guttmann and Peter Höfner

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.

https://www.isa-afp.org/entries/Relational_Paths.html

Enjoy!

smime.p7s

Last updated: Jan 25 2022 at 01:11 UTC