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

A Mechanical Proof of Ramsey’s Theorem via Symbolic Computation

作　　者：鲁健 曾振柄[1] LU Jian;ZENG Zhenbing(Department of Mathematics,Shanghai University,Shanghai 200444;CAS-MPG Partner Institute for Computational Biology,Chinese Academy of Sciences,Shanghai 200031)

机构地区：[1]上海大学理学院数学系,上海200444 [2]中国科学院-德国马普学会计算生物学伙伴研究所,上海200031

出　　处：《系统科学与数学》2021年第12期3311-3323,共13页Journal of Systems Science and Mathematical Sciences

基　　金：国家自然科学基金(12171159,12071282)资助课题。

摘　　要：文章给出Ramsey定理自动证明的一个代数化方法,使用符号计算软件实现了R(3,3)=6和R(3,4)=9的自动证明,并讨论了更复杂情况的简化方法,包括R(3,5)=14和R(3,3,3)=17等情形的分治策略.不同于以往的计算机辅助计算方法,文章将Ramsey定理的转化为多项式的展开合并过程,给出的证明是机械化的.This paper presented a method of algebraic representation of the Ramsey Theorem and gave an implementation for the mechanical proofs to the theorem for two classic cases,i.e.,R(3,3)=6 and R(3,4)=9 using symbolic computation.A divide-and-conquer method was also suggested for tackling with complicated cases including R(3,5)=14 and R(3,3,3)=17.Different from the existed computer aided algorithms,the proposed method can generate mechanical proof of Ramsey theorem through polynomial computation.

关 键 词：Ramsey定理 数学机械化 符号计算 组合优化 分治法 

分 类 号：O157.5[理学—数学]