Verifying minimum spanning tree algorithms with Stone relation algebras

DOI10.1016/j.jlamp.2018.09.005zbMath1401.68247OpenAlexW2892302641WikidataQ128988452 ScholiaQ128988452MaRDI QIDQ1994364

Walter Guttmann

Publication date: 1 November 2018

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2018.09.005

zbMATH Keywords

weighted graphsrelation algebrasformal methodsKleene algebrasStone algebrastotal correctness

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Cylindric and polyadic algebras; relation algebras (03G15) Signed and weighted graphs (05C22)

Related Items

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms, Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL, Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, A Hierarchy of Algebras for Boolean Subsets, FIRST-ORDER AXIOMATISATIONS OF REPRESENTABLE RELATION ALGEBRAS NEED FORMULAS OF UNBOUNDED QUANTIFIER DEPTH, Second-order properties of undirected graphs, Relation-algebraic verification of Borůvka's minimum spanning tree algorithm, Relational characterisations of paths

Uses Software

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

Cites Work

• On the shortest spanning subtree of a graph and the traveling salesman problem
• Relational style laws and constructs of linear algebra
• Internal axioms for domain semirings
• Axiomatizability of positive algebras of binary relations
• Relation algebras by games
• Algebras for iteration and infinite computations
• Abstract abstract reduction
• Relation algebras
• 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
• An algebraic framework for minimum spanning tree problems
• Algebraically closed distributive p-algebras
• 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
• Injective and projective Stone algebras
• Concrete Semantics
• Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
• C-semiring Frameworks for Minimum Spanning Tree Problems
• Relations among Matrices over a Semiring
• Relational Attribute Systems II: Reasoning with Relations in Information Structures
• Regular Algebra Applied to Path-finding Problems
• Representations of ordered semigroups and lattices by binary relations
• Extending Sledgehammer with SMT Solvers
• Stone Relation Algebras
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item