计算机辅助证明有限域上的组合猜想：一个关于国际象棋猜想的案例研究
摘要：使用计算机推导数学证明的方法有几种。为了说明这一点，我们深入研究了使用计算机支持证明一个复杂的组合猜想——国象KRK残局策略的正确性。本文呈现的最终、可机器验证的结果是，对于自然数$n$大于$3$的$n\times n$棋盘来说，白方有获胜策略。我们证明了不同的基于计算机的定理证明方法最好一起配合，并且技术的当前可用性已经足够强大，能够为人类推导复杂的证明提供有力的帮助。
作者：Predrag Janiv{c}i''c, Filip Mari''c, Marko Malikovi''c
论文ID：1801.07528
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22