几何学中的经典证明和机器证明选讲

摘要

数学机器证明是上世纪70年代以来发展起来的一个重要的数学研究领域。本书是捷克数学家所写的一本关于初等几何定理的机器证明的专著。作者基于Groebner基消元理论给出一些著名的初等几何定理和公式的自动证明技术，并应用这些方法发现一些新公式，解决一些几何不等式，完成某些用通常尺规作图不易作出的几何作图。特别是，对于每个问题，作者首先给出自动证明方法，然后给出经典方法（尽可能不使用计算机）让读者比较两种方法的优缺点，从而进一步理解机器证明的基本思想和技术。