Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Kruskal's Algorithm for Minimu...

Email Gateway (Aug 22 2022 at 19:12):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

we have a new contribution, thanks to Maximilian P.L. Haslbeck,
Peter Lammich and Julian Biendarra.

Kruskal's Algorithm for Minimum Spanning Forest

This Isabelle/HOL formalization defines a greedy algorithm for finding a minimum
weight basis on a weighted matroid and proves its correctness. This algorithm is
an abstract version of Kruskal's algorithm. We interpret the abstract algorithm
for the cycle matroid (i.e. forests in a graph) and refine it to imperative
executable code using an efficient union-find data structure. Our formalization
can be instantiated for different graph representations. We provide
instantiations for undirected graphs and symmetric directed graphs.

See https://www.isa-afp.org/entries/Kruskal.html for more details.

Enjoy,
René
signature.asc

Last updated: Apr 19 2024 at 20:15 UTC