Title
Induction with Generalization in Superposition Reasoning.
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.
Year
DOI
Venue
2020
10.1007/978-3-030-53518-6_8
CICM
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
5
Name
Order
Citations
PageRank
Márton Hajdú100.34
Petra Hozzová200.34
Laura Kovács349436.97
Johannes Schoisswohl401.01
Andrei Voronkov52670225.46