Email Gateway (Aug 19 2022 at 11:14): Email Gateway (Aug 19 2022 at 11:14):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
An Axiomatic Characterization of the Single-Source Shortest Path Problem
Christine Rizkallah
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.
http://afp.sourceforge.net/entries/ShortestPath.shtml
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC