Formalizing Graph Trail Properties in Isabelle/HOL

TL;DR

This paper formalizes properties of graph trails in Isabelle/HOL, including algorithms and proofs for trail length bounds in weighted graphs, advancing formal graph theory reasoning.

Contribution

It extends Isabelle/HOL's graph theory library with algorithms and proofs for analyzing decreasing and increasing trails in weighted graphs.

Findings

Proved lower bounds on trail lengths in weighted graphs

Extended Isabelle/HOL with algorithms for longest decreasing trails

Established that decreasing trails are also increasing

Abstract

We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one. This preprint has been accepted for publication at CICM 2020.