一句话：为 McKay–Piperno 图规范标号算法构建形式证明系统，导出可独立检查的证明以验证图非异构。
在交互式定理证明器中使用图规范标号与同构检查时，算法要么经过机器验证，要么其结果可由独立检查器验证。本文分析 McKay 与 Piperno 的先进图规范标号算法，将其表述为一个形式证明系统，并实现可导出给定图规范形式证明的工具。导出的证明由独立检查器验证，从而可确认两个图不同构。该工作把规范标号算法的正确性证据转化为可检查证明，为在定理证明环境中可靠使用图同构与非同构检查提供了基础。
In order to apply canonical labelling of graphs and isomorphism checking in interactive theorem provers, these checking algorithms must either be mechanically verified or their results must be verifiable by independent checkers. We analyze a state-of-the-art algorithm for canonical labelling of graphs (described by McKay and Piperno) and formulate it in terms of a formal proof system. We provide an implementation that can export a proof that the obtained graph is the canonical form of a given graph. Such proofs are then verified by our independent checker and can be used to confirm that two given graphs are not isomorphic.
@article{paperbot2241,
title = {A proof system for graph (non)-isomorphism verification},
author = {Milan Banković and Ivan Drecun and Filip Marić},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:9)2023}
}