论文标题
在Double-Pushout图形转换中迈向机械化的证明
Towards Mechanised Proofs in Double-Pushout Graph Transformation
论文作者
论文摘要
我们正式化了双线助理助手Isabelle/Hol中图形转换的基础知识，并提供了相关的机器检查证明。具体而言，我们将图形，图形形态和规则形式化，以及基于删除和粘合的直接派生的定义。然后，我们将图形下降正式化，并在Isabelle的帮助下证明了删除和粘合物都是下定位的。我们还证明了下定位是独一无二的同构。形式化包括约2000行源文本。我们的动机是为双线图理论中的严格，机器检查的证明铺平道路，并通过交互式定理证明验证图形转换系统和基于规则的图形程序的基础。
We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition of direct derivations based on deletion and gluing. We then formalise graph pushouts and prove with Isabelle's help that both deletions and gluings are pushouts. We also prove that pushouts are unique up to isomorphism. The formalisation comprises around 2000 lines of source text. Our motivation is to pave the way for rigorous, machine-checked proofs in the theory of the double-pushout approach, and to lay the foundations for verifying graph transformation systems and rule-based graph programs by interactive theorem proving.
