Aggregation Algebras

Walter Guttmann 🌐

September 15, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

BSD 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

Depends on

Used by

Cite

× 
@article{Aggregation_Algebras-AFP,
  author  = {Walter Guttmann},
  title   = {Aggregation Algebras},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2018},
  note    = {\url{https://isa-afp.org/entries/Aggregation_Algebras.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: