有限域上组合猜想的计算机辅助证明：以国际象棋猜想为例
计算机科学中的逻辑
2023-06-22 v4
摘要
利用计算机推导数学证明有若干种途径。为加以说明，我们深入研究了利用计算机辅助证明一个复杂组合猜想——国际象棋 KRK 残局策略的正确性。本文给出的最终经机器可验证的结果是：在推广至 棋盘（对大于 的自然数 ）的 KRK 残局中，白方存在必胜策略。我们论证了不同的基于计算机的定理证明方法协同配合效果最佳，且当前可用技术已足够强大，能为人类推导复杂证明提供实质性帮助。
引用
@article{arxiv.1801.07528,
title = {Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture},
author = {Predrag Janičić and Filip Marić and Marko Maliković},
journal= {arXiv preprint arXiv:1801.07528},
year = {2023}
}