面向双推图变换的机械化和证明
计算机科学中的逻辑
2022-12-23 v1
摘要
我们在证明辅助工具 Isabelle/HOL 中形式化了双推（double-pushout）图变换方法的基础，并提供了相关的机器检查证明。具体而言，我们形式化了图、图态射与规则，以及基于删除与粘合的直接推导定义。随后我们形式化了图推挽并借助 Isabelle 证明删除与粘合均为推挽。我们还证明了推挽在同构意义下唯一。该形式化包含约 2000 行源文本。我们的动机是为双推方法理论中的严格机器检查证明铺平道路，并为通过交互式定理证明验证图变换系统与基于规则的图程序奠定基础。
引用
@article{arxiv.2212.11630,
title = {Towards Mechanised Proofs in Double-Pushout Graph Transformation},
author = {Robert Söldner and Detlef Plump},
journal= {arXiv preprint arXiv:2212.11630},
year = {2022}
}
备注
In Proceedings GCM 2022, arXiv:2212.10975