Abstract
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.
License
Topics
Session Kruskal
- Kruskal_Misc
- SeprefUF
- MinWeightBasis
- Kruskal
- Kruskal_Refine
- Kruskal_Impl
- UGraph
- UGraph_Impl
- Graph_Definition
- Graph_Definition_Aux
- Graph_Definition_Impl