在 Isabelle/HOL 中形式化图迹性质
计算机科学中的逻辑
2021-03-08 v1
摘要
我们描述了一个使用 Isabelle/HOL 表达并证明图迹性质的数据集。我们利用边上的权值形式化了关于严格递增与严格递减迹的推理，并证明了加权图中迹长度的下界。为此，我们通过一种计算给定权值分布下从某顶点出发的最长严格递减图迹长度的算法扩展了 Isabelle/HOL 的图论库，并证明任何递减迹也是递增迹。本预印本已被 CICM 2020 接收发表。
关键词
引用
@article{arxiv.2103.03607,
title = {Formalizing Graph Trail Properties in Isabelle/HOL},
author = {Laura Kovacs and Hanna Lachnitt and Stefan Szeider},
journal= {arXiv preprint arXiv:2103.03607},
year = {2021}
}