形式化 Frankl 猜想：FC-族
离散数学
2012-07-17 v1
摘要
Frankl 猜想提出于 1979 年，至今仍未解决，它指出在每个对并运算封闭的集族中，存在一个元素包含在至少一半的集合中。FC-族是指已被证明满足以下条件的集族：任何包含它们的并封闭集族都满足 Frankl 条件（例如，在任何包含单元素集 {a} 的并封闭集族中，元素 a 包含在至少一半的集合中，因此形如 {a} 的集族是最简单的 FC-族）。FC-族在攻克 Frankl 猜想中起着重要作用，因为它们能够显著剪枝搜索空间。我们提出了一种用于证明某集族为 FC-族的计算机辅助方法的形式化。该方法采用“通过计算证明”的范式，并使用证明助手 Isabelle/HOL 来检查数学内容，并执行证明所依赖的（已验证的）组合搜索。我们确认了文献中已知的 FC-族，并发现了一个新的 FC-族。
引用
@article{arxiv.1207.3604,
title = {Formalizing Frankl's Conjecture: FC-families},
author = {Filip Marić and Miodrag Živković and Bojan Vučković},
journal= {arXiv preprint arXiv:1207.3604},
year = {2012}
}
备注
Intelligent Computer Mathematics (CICM 2012). Calculemus track. LNAI 7362, Springer, 2012