Relational Minimum Spanning Tree Algorithms

Walter Guttmann 🌐 and Nicolas Robinson-O’Brien

December 8, 2020

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 verify the correctness of Prim's, Kruskal's and Borůvka's minimum spanning tree algorithms based on algebras for aggregation and minimisation.

License

BSD License

Topics

Session Relational_Minimum_Spanning_Trees

Depends on

Cite

× 
@article{Relational_Minimum_Spanning_Trees-AFP,
  author  = {Walter Guttmann and Nicolas Robinson-O'Brien},
  title   = {Relational Minimum Spanning Tree Algorithms},
  journal = {Archive of Formal Proofs},
  month   = {December},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: