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.
翻译:为了应用图表的金字塔标签和在交互式理论验证器中进行非形态式检查,这些核对算法必须经过机械核查,或者其结果必须由独立的检查器进行核查。我们分析了图表(由麦凯和皮佩诺描述的)的卡通式标签的最新算法,并以正式的验证系统来编制。我们提供了一个执行程序,可以输出一个证据,证明所获得的图表是某一图表的卡通式形式。这些证据随后由我们的独立检查器进行核查,并可用于确认两个给定的图表不是无形态的。