An Axiomatic Characterization of the Single-Source Shortest Path Problem

Title:	An Axiomatic Characterization of the Single-Source Shortest Path Problem
Author:	Christine Rizkallah
Submission date:	2013-05-22
Abstract:	This theory is split into two sections. In the first section, we give a formal proof that a well-known axiomatic characterization of the single-source shortest path problem is correct. Namely, we prove that in a directed graph with a non-negative cost function on the edges the single-source shortest path function is the only function that satisfies a set of four axioms. In the second section, we give a formal proof of the correctness of an axiomatic characterization of the single-source shortest path problem for directed graphs with general cost functions. The axioms here are more involved because we have to account for potential negative cycles in the graph. The axioms are summarized in three Isabelle locales.
BibTeX:	@article{ShortestPath-AFP, author = {Christine Rizkallah}, title = {An Axiomatic Characterization of the Single-Source Shortest Path Problem}, journal = {Archive of Formal Proofs}, month = may, year = 2013, note = {\url{https://isa-afp.org/entries/ShortestPath.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Graph_Theory
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.