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 条
  • [1] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
  • [2] Formalizing provable anonymity in Isabelle/HOL
    Li, Yongjian
    Pang, Jun
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (02) : 255 - 282
  • [3] Formalizing rewriting introduction on Isabelle/HOL
    Kimura Y.
    Aoto T.
    Computer Software, 2020, 37 (02) : 104 - 119
  • [4] Formalizing IMO Problems and Solutions in Isabelle/HOL
    Maric, Filip
    Stojanovic-Durdevic, Sana
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (328): : 35 - 55
  • [5] Formalizing Jordan Normal Forms in Isabelle/HOL
    Thiemann, Rene
    Yamada, Akihisa
    PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 88 - 99
  • [6] Formalizing Coppersmith's Method in Isabelle/HOL
    Kosaian, Katherine
    Tan, Yong Kiam
    Rozier, Kristin Yvonne
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2024, 2024, 14690 : 127 - 145
  • [7] Formalizing Pick's Theorem in Isabelle/HOL
    Binder, Sage
    Kosaian, Katherine
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2024, 2024, 14690 : 109 - 126
  • [8] Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
    From, Asta Halkjaer
    Eschen, Agnes Moesgard
    Villadsen, Jorgen
    INTELLIGENT COMPUTER MATHEMATICS (CICM 2021), 2021, 12833 : 32 - 46
  • [9] Formalizing Ordinal Partition Relations Using Isabelle/HOL
    Dzamonja, Mirna
    Koutsoukou-Argyraki, Angeliki
    Paulson, Lawrence C.
    EXPERIMENTAL MATHEMATICS, 2022, 31 (02) : 383 - 400
  • [10] Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL
    Hess, Andreas Viktor
    Modersheim, Sebastian
    2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 451 - 463
12345