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.
翻译：我们用Isabelle/HOL来描述一组表示和证明图表路径属性的数据集。 我们正式确定关于严格增加和减少线索的推理,使用边上的重量,并证明加权图表中线索长度的下限。 我们这样做的方法是扩展Isabelle/HOL的图形理论库,从某一重量分布的顶点开始,计算一个最长、严格缩短的图表路径长度的算法,并证明任何减少的路径也越来越长。 这个预印已被接受,供在2020年CICM出版。
相关内容
微信扫码咨询专知VIP会员