使用Rocq证明器和mathcomp/ssreflect对Sands-Sauer-Woodrow定理的形式化证明
离散数学
2026-04-24 v1
摘要
我们使用Rocq证明助手和MathComp/SSReflect库给出了Sands-Sauer-Woodrow (SSW)定理的形式化证明。SSW定理指出，在一个边用两种颜色着色且没有单色无限外向路径的有向图中，存在一个顶点独立集S，使得S外的每个顶点都可以通过一条单色路径到达S。我们使用两个二元关系Eb和Er（分别表示蓝色和红色边）来形式化该图，并开发了一个用于表示为经典集合的二元关系的专用库。除了形式化原始的SSW定理，我们还建立了一个严格更强的版本，其中假设“没有单色无限外向路径”被替换为更弱的条件，即Eb和Er的传递闭包的非对称部分没有无限外向路径。然后，通过一个引理（表明关系的传递闭包的非对称部分的无限路径意味着该关系的无限路径），原始SSW定理作为推论被恢复。
引用
@article{arxiv.2604.21376,
title = {A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect},
author = {Jean-Philippe Chancelier},
journal= {arXiv preprint arXiv:2604.21376},
year = {2026}
}