Abstract
We develop algebras for aggregation and minimisation for weight
matrices and for edge weights in graphs. We verify the correctness of
Prim's and Kruskal's minimum spanning tree algorithms based
on these algebras. We also show numerous instances of these algebras
based on linearly ordered commutative semigroups.
License
History
- December 9, 2020
- moved Hoare logic to HOL-Hoare, moved spanning trees to Relational_Minimum_Spanning_Trees (revision dbb9bfaf4283)
Topics
Session Aggregation_Algebras
- Semigroups_Big
- Aggregation_Algebras
- Matrix_Aggregation_Algebras
- Linear_Aggregation_Algebras
- M_Choose_Component