-
A proof system for graph (non)-isomorphism verification
Abstract: 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 a… ▽ More
Submitted 31 January, 2023; v1 submitted 28 December, 2021; originally announced December 2021.
ACM Class: F.4.1
Journal ref: Logical Methods in Computer Science, Volume 19, Issue 1 (February 1, 2023) lmcs:8898