Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

**Jing-Chao Chen**- Donghua University, Shanghai
**Yatsuka Nakamura**- Shinshu University, Nagano

- A path from a source vertex $v$ to a target vertex $u$ is said to be a shortest path if its total cost is minimum among all $v$-to-$u$ paths. Dijkstra's algorithm is a classic shortest path algorithm, which is described in many textbooks. To justify its correctness (whose rigorous proof will be given in the next article), it is necessary to clarify its underlying principle. For this purpose, the article justifies the following basic facts, which are the core of Dijkstra's algorithm. \begin{itemize} \itemsep-3pt \item A graph is given, its vertex set is denoted by $V.$ Assume $U$ is the subset of $V,$ and if a path $p$ from $s$ to $t$ is the shortest among the set of paths, each of which passes through only the vertices in $U,$ except the source and sink, and its source and sink is $s$ and in $V,$ respectively, then $p$ is a shortest path from $s$ to $t$ in the graph, and for any subgraph which contains at least $U,$ it is also the shortest. \item Let $p(s,x,U)$ denote the shortest path from $s$ to $x$ in a subgraph whose the vertex set is the union of $\{s,x\}$ and $U,$ and cost $(p)$ denote the cost of path $p(s,x,U),$ cost$(x,y)$ the cost of the edge from $x$ to $y.$ Give $p(s,x,U),$ $q(s,y,U)$ and $r(s,y,U \cup \{x\})$. If ${\rm cost}(p) = {\rm min} \{{\rm cost}(w): w(s,t,U) \wedge t \in V\}$, then we have $${\rm cost}(r) = {\rm min} ({\rm cost}(p)+{\rm cost}(x,y),{\rm cost}(q)).$$ \end{itemize} \noindent This is the well-known triangle comparison of Dijkstra's algorithm.

- Preliminaries
- Additional Properties of Finite Sequences
- Additional Properties of Chains and Oriented Paths
- Additional Properties of Acyclic Oriented Paths
- The Set of the Vertices On a Path or an Edge
- Directed Paths between Two Vertices
- Acyclic (or Simple) Paths
- Weight Graphs and Their Basic Properties
- Shortest Paths and Their Basic Properties
- Basic Properties of a Graph with Finite Vertices
- Three Basic Theorems for Dijkstra's Shortest Path Algorithm

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
*Journal of Formalized Mathematics*, 2, 1990. - [7]
Czeslaw Bylinski.
The sum and product of finite sequences of real numbers.
*Journal of Formalized Mathematics*, 2, 1990. - [8]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Krzysztof Hryniewiecki.
Graphs.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Jaroslaw Kotowicz and Yatsuka Nakamura.
Introduction to Go-Board --- part I.
*Journal of Formalized Mathematics*, 4, 1992. - [12]
Yatsuka Nakamura and Piotr Rudnicki.
Oriented chains.
*Journal of Formalized Mathematics*, 10, 1998. - [13]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [14]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [15]
Wojciech A. Trybulec.
Pigeon hole principle.
*Journal of Formalized Mathematics*, 2, 1990. - [16]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [17]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]