Email Gateway (Aug 23 2022 at 09:26): Email Gateway (Aug 23 2022 at 09:26):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: Nov 21 2024 at 12:39 UTC