Dilworth 定理与 Mirsky 定理的完全机械化证明
计算机科学中的逻辑
2017-03-20 v1 离散数学
摘要
我们在 Coq 证明助手中给出了 Dilworth 定理和 Mirsky 定理的两个完全机械化证明。Dilworth 定理指出，在任何有限偏序集（poset）中，最小链覆盖的大小与最大反链的大小相同。Mirsky 定理是 Dilworth 定理的对偶定理。我们形式化了 Perles [2]（针对 Dilworth 定理）和 Mirsky [5]（针对对偶定理）的证明。我们还构建了一个定义和事实库，可作为形式化其他有限偏序集定理的框架。
引用
@article{arxiv.1703.06133,
title = {Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem},
author = {Abhishek Kr Singh},
journal= {arXiv preprint arXiv:1703.06133},
year = {2017}
}