### 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

- Mathematics/Algebra

### Session Aggregation_Algebras

- Semigroups_Big
- Aggregation_Algebras
- Matrix_Aggregation_Algebras
- Linear_Aggregation_Algebras
- M_Choose_Component

### Depends on

- Stone-Kleene Relation Algebras

### Used by

- Relational Disjoint-Set Forests

## Cite

×

Aggregation_Algebras-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Sep 16, 2018 : Isabelle2018