机器证明理论和算法

中国科学院成都计算机应用研究所张景中、杨路等完成。该研究给出了世界上第一个能够自动产生几何定理的可读证明的算法和程序，使这一多年未能解决的难题得以突破。用Lisp语言写的程序在NEXT工作站上成功地产生了400多条非平凡的几何定理的可读证明，其中不少证明简短而优美。提出并实现定理机器证明《数值并行法》，研制成功 《L类定理自动证明机》。对 “等式型几何定理” 通过有限次数值检验加以严格证明有效算法，占用内存极少，在国际上首次实现了用袖珍微机 (如PC700)证明非平凡几何定理以及发现新定理。该法采用几何语句作为输入，不需作任何数学上的技术处理。彻底解决了非线性代数系统相关性判定问题。用吴除法和子结式计算建立了升列组的WR分解法，彻底解决了可约升列相对分解问题，并改进了著名 的吴氏非退化条件。运用上述独创的新算法和自制软件所发现的几何新定理，已引起国际同行注目并展开讨论。机器证明领域国际权威学者对该研究成果给予高度评价。获1995年中国科学院自然科学奖一等奖。