Formalizing Graph Trail Properties in Isabelle/HOL

被引：0
|
作者：
Kovacs, Laura [1 ]
Lachnitt, Hanna [1 ]
Szeider, Stefan [1 ]
机构：
[1] TU Wien, Vienna, Austria
来源：
INTELLIGENT COMPUTER MATHEMATICS, CICM 2020 | 2020年 / 12236卷
关键词：
Weighted graph; Increasing/decreasing trails; Isabelle/HOL; Verified theory formalization; MONOTONE PATHS;
D O I：
10.1007/978-3-030-53518-6_12
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
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.
引用
收藏
页码：190 / 205
页数：16
相关论文
共 50 条
  • [31] Data Refinement in Isabelle/HOL
    Haftmann, Florian
    Krauss, Alexander
    Kuncar, Ondrej
    Nipkow, Tobias
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 100 - 115
  • [32] From LCF to Isabelle/HOL
    Paulson, Lawrence C.
    Nipkow, Tobias
    Wenzel, Makarius
    FORMAL ASPECTS OF COMPUTING, 2019, 31 (06) : 675 - 698
  • [33] Linear Resources in Isabelle/HOL
    Smola, Filip
    Fleuriot, Jacques D.
    JOURNAL OF AUTOMATED REASONING, 2024, 68 (02)
  • [34] Nominal techniques in Isabelle/HOL
    Urban, C
    Tasson, C
    AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 38 - 53
  • [35] Markov Processes in Isabelle/HOL
    Hoelz, Johannes
    PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17, 2017, : 100 - 111
  • [36] A Consistent Foundation for Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    INTERACTIVE THEOREM PROVING, 2015, 9236 : 234 - 252
  • [37] A Consistent Foundation for Isabelle/HOL
    Ondřej Kunčar
    Andrei Popescu
    Journal of Automated Reasoning, 2019, 62 : 531 - 555
  • [38] Nominal techniques in isabelle/HOL
    Urban, Christian
    Journal of Automated Reasoning, 2008, 40 (04): : 327 - 356
  • [39] A Consistent Foundation for Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    JOURNAL OF AUTOMATED REASONING, 2019, 62 (04) : 531 - 555
  • [40] Owicki/Gries in Isabelle/HOL
    Nipkow, T
    Nieto, LP
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 1999, 1577 : 188 - 203
12345