首页> 外文会议>International Conference on Intelligent Computer Mathematics >Formalizing Graph Trail Properties in Isabelle/HOL
【24h】

Formalizing Graph Trail Properties in Isabelle/HOL

机译:在Isabelle / HOL中正式化图迹属性

获取原文

摘要

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.
机译:我们使用Isabelle / HOL描述了一个表示和证明图迹特性的数据集。我们使用边上的权重,对严格增加和减少轨迹的推理进行形式化,并证明加权图中轨迹长度的下界。为此,我们使用一种算法来扩展Isabelle / HOL的图形理论库,该算法可计算从给定权重分布的顶点开始的最长严格减少的图形轨迹的长度,并证明任何减少的轨迹也都是递增的。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号