Milan Banković ; Ivan Drecun ; Filip Marić - A proof system for graph (non)-isomorphism verification

lmcs:8898 - Logical Methods in Computer Science, February 1, 2023, Volume 19, Issue 1 - https://doi.org/10.46298/lmcs-19(1:9)2023
A proof system for graph (non)-isomorphism verificationArticle

Authors: Milan Banković ORCID; Ivan Drecun ; Filip Marić

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.

https://doi.org/10.46298/lmcs-19(1:9)2023
Source: arXiv.org:2112.14303
Volume: Volume 19, Issue 1
Published on: February 1, 2023
Accepted on: January 17, 2023
Submitted on: December 30, 2021
Keywords: Computer Science - Logic in Computer Science, F.4.1
Licence: Attribution 4.0 International (CC BY 4.0)
Funding:
    Source : OpenAIRE Graph
  • Automated Reasoning and Data Mining; Funder: Ministry of Education, Science and Technological Development of Republic of Serbia; Code: 174021

Publications

Has review
  • 1 zbMATH Open

1 Document citing this article

Share and export

Consultation statistics

This page has been seen 2560 times.
This article's PDF has been downloaded 2743 times.