用符号计算证明Ramsey定理的一个机械化方法

作者：鲁健; 曾振柄^*

来源：系统科学与数学, 2021, 41(12): 3311-3323.

• Ramsey定理
• 数学机械化
• 符号计算
• 组合优化
• 分治法

文章给出Ramsey定理自动证明的一个代数化方法,使用符号计算软件实现了R(3,3)=6和R(3,4)=9的自动证明,并讨论了更复杂情况的简化方法,包括R(3,5)=14和R(3,3,3)=17等情形的分治策略.不同于以往的计算机辅助计算方法,文章将Ramsey定理的转化为多项式的展开合并过程,给出的证明是机械化的.

• 单位
  中国科学院; 上海大学