# Formalizing Graph Trail Properties in Isabelle/HOL

arXiv: https://arxiv.org/abs/2103.03607 · HTML: https://mlsanity.com/paper/2103.03607/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2021.

## Built on by (most cited first, 2 of 2)

- [Can LLM Aid in Solving Constraints with Inductive Definitions?](https://mlsanity.com/paper/2603.03668/) (2026)
- [Conjectures, Tests and Proofs: An Overview of Theory Exploration](https://mlsanity.com/paper/2109.03721/) (2021)

## Abstract (arXiv)

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.