一句话：在 Isabelle/HOL 中形式化双推出图变换基础理论，并机器验证推导唯一性与 Church-Rosser 定理。
本文在 Isabelle/HOL 中为双推出（DPO）图变换的基础理论建立形式化框架。作者定义了图、态射、推出与拉回等核心概念，证明其基本性质，并基于 Rosens（1975）的工作建立推导唯一性，借助 Ehrig 与 Kreowski（1976）的证明验证 Church-Rosser 定理，从而表明该形式化方法的有效性。论文还详细介绍了采用 Isabelle/HOL 的方法论、影响当前版本的关键设计决策，以及在高阶逻辑中应用交互式定理证明器所涉及的技术复杂性，旨在让读者深入理解形式化验证工具在澄清复杂数学概念方面日益重要的作用。
In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts.
@article{paperbot2716,
title = {Formalising the Double-Pushout Approach to Graph Transformation},
author = {Robert Söldner and Detlef Plump},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:3)2024}
}