数学机械化研究中的例证法

1986年，洪加威发表了他的著名成果，即例证法：为了判定一个一般的几何命题是否正确，只需计算一个具体的数值特例并且精确到指定的有效位数就行。一些人(如王东明等)对之作了改进，但洪的算法基本不能在计算机上实现。后来，张景中、杨路提出了有效的多点例证法，侯晓荣提出了有效的单点例证法等。国外也有相关的研究，如半数值的柱形代数剖分算法、非严格的概率数值算法等。这些研究只对初等几何(特别是等式型)命题有效。本项目致力于把例证法推广于更大的范围，特别是在数学机械化研究中比较困难的不等式和非初等命题的自动证明。不等式的证明一直是数学机械化研究中的老大难问题，近年来虽有不少的进展，但基本依赖于困难的符号运算，只能处理一些少参数的情形。本项目旨在研究全新的、并行的例证法，以使例证法能解决一些真正困难的问题(包括一些公开问题)；也将研究非初等领域的例证法而超越此前的相关研究。