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.
翻译：我们正式化了校对助理Isabelle/HOL对图形转换的双推法的基本原理,并提供了相关的机检证明。具体地说,我们正式化了图表、图形形态和规则,并定义了基于删除和粘贴的直接衍生物。然后我们正式化了图表推出,并在Isabelle的帮助下证明,删除和凝胶都是推出。我们还证明推出是非无貌化的独特方法。正式化包括了大约2000行源文本。我们的动机是,在双推法理论中,为严格、机检的验证铺平道路,并通过互动理论验证,为核实图形转换系统和基于规则的图形程序奠定基础。
相关内容
微信扫码咨询专知VIP会员