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

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session ShortestPath

- ShortestPath
- ShortestPathNeg

### Depends on

- Graph Theory

### Auto-related entries

- Euler’s Polyhedron Formula
- Wetzel’s Problem and the Continuum Hypothesis
- Lucas’s Theorem
- The number of comparisons in QuickSort
- The Cartan Fixed Point Theorems

## Cite

×

ShortestPath-AFP

    @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},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- May 30, 2013 : Isabelle2013