有限集组合学中若干核心定理的形式化
计算机科学中的逻辑
2019-12-13 v1 离散数学
摘要
我们给出了组合学中若干核心定理的完全形式化证明。这些定理包括 Dilworth 分解定理、Mirsky 定理、Hall 婚姻定理和 Erd\H{o}s-Szekeres 定理。Dilworth 分解定理是其中的关键结果。它指出，在任何有限偏序集 (poset) 中，最小链覆盖的大小与最大反链的大小相同。Mirsky 定理是 Dilworth 分解定理的对偶，它指出在任何有限偏序集中，最小反链覆盖的大小与最大链的大小相同。我们在 Hall 婚姻定理和 Erd\H{o}s-Szekeres 定理的证明中使用了 Dilworth 定理。这些定理涉及的组合对象是集合与序列。所有证明均在 Coq 证明助手中进行了形式化。我们开发了一个定义与事实库，可作为形式化有限偏序集其他定理的框架。
引用
@article{arxiv.1703.10977,
title = {Formalization of some central theorems in combinatorics of finite sets},
author = {Abhishek Kr Singh},
journal= {arXiv preprint arXiv:1703.10977},
year = {2019}
}
备注
arXiv admin note: substantial text overlap with arXiv:1703.06133