全自动验证分类所有 Frankl-完全（FC(6)）集族
计算机科学中的逻辑
2019-02-26 v1 离散数学
摘要
Frankl 猜想于 1979 年提出且至今未解，其断言在每一个对并运算封闭的集族中，存在一个元素出现在至少一半的集合中。若对于每一个包含 Fc 的并封闭族 F，Fc 的并中某个元素出现在 F 至少一半的元素中（即 F 满足 Frankl 条件），则称族 Fc 为 Frankl-完全（或 FC-族）。FC-族在攻克 Frankl 猜想中起着重要作用，因为它们能显著剪枝搜索空间。我们通过定义并枚举所有极小 FC 族与极大非 FC 族，给出了 6 元素全集上所有 FC-族的总体刻画，扩展了先前工作。我们采用全自动化、计算机辅助的方法，并在证明辅助工具 Isabelle/HOL 中形式化验证。
引用
@article{arxiv.1902.08765,
title = {Fully Automatic, Verified Classification of all Frankl-Complete (FC(6)) Set Families},
author = {Filip Marić and Bojan Vučković and Miodrag Živković},
journal= {arXiv preprint arXiv:1902.08765},
year = {2019}
}