摘要： 在几何定理的机器证明中,遇到可约的情形就会出现重大困难。本文依据代数几何中代数簇相对可约与绝对可约的概念,引进直线与园的定向座标,以避免或至少减轻可约性的困难。作为应用实例,我们对割线定理、Feuerbah 定理以及 Thebault-Taglor-Chou 定理进行了分析,并对最后一个定理给出了比已知要简单得多的机器证明。
吴文俊. 初等几何定理机器证明中的可约性问题[J]. 数学季刊, 1987, 2(2): 1-20.
WU Wen-tsun. On Reducibility Problem in Mechanical Theorem Proving of Elementary Geometies [J]. Chinese Quarterly Journal of Mathematics, 1987, 2(2): 1-20.
