|
|||||
|
|
| 用符号计算证明Ramsey定理的一个机械化方法 | |
| 引用本文： | 鲁健,曾振柄.用符号计算证明Ramsey定理的一个机械化方法[J].系统科学与数学,2021(12):3311-3323. |
| 作者姓名： | 鲁健 曾振柄 |
| 作者单位： | 1. 上海大学理学院数学系;2. 中国科学院-德国马普学会计算生物学伙伴研究所 |
| 基金项目： | 国家自然科学基金(12171159,12071282)资助课题； |
| 摘 要： | 文章给出Ramsey定理自动证明的一个代数化方法,使用符号计算软件实现了R(3,3)=6和R(3,4)=9的自动证明,并讨论了更复杂情况的简化方法,包括R(3,5)=14和R(3,3,3)=17等情形的分治策略.不同于以往的计算机辅助计算方法,文章将Ramsey定理的转化为多项式的展开合并过程,给出的证明是机械化的. |
| 关 键 词： | Ramsey定理 数学机械化 符号计算 组合优化 分治法 |