Formalizing graph trail properties

Abstract

We survey two methods to reason about ordered trails in edge-weighted graphs. Firstly, we provide an encoding in first-order logic in order to apply automated theorem provers to the problem. Conducting experiments on the size of the input instance, we show the disadvantages of this approach. Motivated by this we present a symbolic proof of the lower bound on the length of strictly ordered trails in weighted graphs. Then, we formalize strictly ordered trails in the proof assistant Isabelle/HOL. We express and prove properties of these trails and verify the lower bounds on the length in Isabelle. 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 in an undirected graph any decreasing trail is also an increasing one. We also present a symbolic proof that shows an upper bound on the minimum length of strictly ordered trails. To this end we present an algorithm to construct graphs that witness the upper bound an implementation of this algorithm.

Wir prüfen zwei verschiedene Methoden um automatisch über streng monotone fallende oder streng monoton steigende Kantenzüge in kantengewichteten Graphen zu argumentieren. Zunächst präsentieren wir eine Formulierung als prädikatenlogisches Problem und evaluieren die Anwendung automatischer Theorembeweiser. Wir zeigen die Nachteile dieses Ansatzes, durch experimentelle Auswertung der Abhängigkeit der gebrauchten Zeit von der Größe des Graphen. Motiviert von diesen Einschränkungen präsentieren wir einen Beweis für eine untere Grenze der Länge von streng monotonen Kantenzügen, der nicht von der Größe des Graphen abhängt. Wir formalisieren Eigenschaften streng monoton fallender und streng monoton steigender Kantenzüge im Beweisassistenen Isabelle/HOL und verifizieren den Beweis der unteren Grenze der Länge des längsten streng monoton fallenden Kantenzugs. Dafür erweitern wir Isabelles Bibliothek für Graphentheorie mit einem Algorithmus, der die Länge des längsten streng monoton fallenden Kantenzugs von einem Knoten für eine gegebene Verteilung der Kantengewichte berechnet. Des Weiteren beweisen wir in Isabelle, dass in einem ungerichtetem Graphen jeder streng monoton fallende Kantenzug auch ein streng monoton steigender Kantenzug ist. Außerdem präsentieren wir einen konstruktiven Beweis, der eine obere Grenze der minimalen Länge eines streng monotonen Kantenzug in vollständigen Graphen zeigt. Im Zuge dessen geben wir auch einen Algorithmus zur Erzeugung von vollständigen Graphen beliebiger Größe an, die zeigen, dass Graphen mit einer bestimmten maximalen Länge von Kantenzügen existieren.