Aggregation Algebras

Walter Guttmann

15 September 2018


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.
BSD License

Change history

[2020-12-09] moved Hoare logic to HOL-Hoare, moved spanning trees to Relational_Minimum_Spanning_Trees (revision dbb9bfaf4283)

Depends On

Used by


Related Entries