图的（非）同构验证的证明系统
摘要：图的规范标签化和同构检查是交互式定理证明器中的重要应用。这些检查算法必须经过机械验证，或者它们的结果必须可由独立检查者验证。我们分析了McKay和Piperno提出的一种先进的图的规范标签化算法，并将其表述为一个形式化证明系统。我们提供了一个实现，可以导出一个给定图形的规范形式的证明。这些证明然后由我们的独立检查器进行验证，并可用于确认两个给定的图形是不同构的。
作者：Milan Bankovi''c, Ivan Drecun, Filip Mari''c
论文ID：2112.14303
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22