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 条
  • [21] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [22] Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem
    Kharim, Aabid Seeyal Abdul
    Prathamesh, T. V. H.
    Rajiv, Shweta
    Vyas, Rishi
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2023, 2023, 14101 : 158 - 173
  • [23] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [24] Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL
    Soualah, Sohaib
    Khalgui, Mohamed
    Chaoui, Allaoua
    ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 2, AINA 2024, 2024, 200 : 199 - 212
  • [25] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
  • [26] On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study
    Bittner, Thomas
    APPLIED ONTOLOGY, 2019, 14 (03) : 251 - 292
  • [27] Unifying Theories in Isabelle/HOL
    Feliachi, Abderrahmane
    Gaudel, Marie-Claude
    Wolff, Burkhart
    UNIFYING THEORIES OF PROGRAMMING, 2010, 6445 : 188 - +
  • [28] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [29] Nominal techniques in Isabelle/HOL
    Urban, Christian
    JOURNAL OF AUTOMATED REASONING, 2008, 40 (04) : 327 - 356
  • [30] A comparison of PVS and Isabelle/HOL
    Griffioen, D
    Huisman, M
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 123 - 142
12345