Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm

DOI10.1007/978-3-319-46750-4_4zbMath1400.68155OpenAlexW2521096248MaRDI QIDQ3179390

Walter Guttmann

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-46750-4_4

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Graph algorithms (graph-theoretic aspects) (05C85) Signed and weighted graphs (05C22)

Related Items (7)

Stone Relation Algebras ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Pseudocomplementation and minimal prime ideals in semirings ⋮ Unnamed Item ⋮ Relation-algebraic verification of Borůvka's minimum spanning tree algorithm ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ An algebraic framework for minimum spanning tree problems

Uses Software

• Isabelle
• RelView
• Isabelle/HOL
• HOL
• Sledgehammer
• Archive Formal Proofs
• Relation Algebra
• Kleene Algebra

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• Relational style laws and constructs of linear algebra
• The saga of minimum spanning trees
• Abstract abstract reduction
• The verified incremental design of a distributed spanning tree algorithm: Extended abstract
• Winskel is (almost) right: Towards a mechanized semantics textbook
• A completeness theorem for Kleene algebras and the algebra of regular events
• Relation-algebraic semantics
• Isabelle/HOL. A proof assistant for higher-order logic
• A new algebraic approach to L-fuzzy relations convenient to study crispness
• Lattices and ordered algebraic structures
• Towards a linear algebra of programming
• Dijkstra, Floyd and Warshall meet Kleene
• Categorical representation theorems of fuzzy relations
• Computing tournament solutions using relation algebra and RelView
• Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures
• A linear algebra approach to OLAP
• Graphs, dioids and semirings. New models and algorithms.
• L-fuzzy sets
• C-semiring Frameworks for Minimum Spanning Tree Problems
• Extended Static Checking by Calculation Using the Pointfree Transform
• Extending Sledgehammer with SMT Solvers
• WEIGHTED AUTOMATA AS COALGEBRAS IN CATEGORIES OF MATRICES
• On the Cardinality of Relations

This page was built for publication: Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm