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

Pavel Pech University of South Bohemia,

Czech Republic

Selected Topics in Geometry

With Classical VS.

Computer Proving

2007, 239pp.

Hardcover

ISBN 9789812709424

P.沛赫著

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

全书含9章。1.引论,概述了机器证明的意义、思想和历史;2.定理自动证明,给出本书的理论基础,主要是代数几何的一些基本概念和结果,以及自动推导和自动发现的基本原理;3-9.对于某些精心选择的重要的著名的初等几何定理和公式逐一给出自动证明和经典证明,并加以评注,其中包括:三解形和四边形的面积公式(Heron公式和Staudt公式)及它们的推广;SimsonMWallece三垂足共线定理及推广;多边形的横截定理(Ceva定理、Menelaus定理、Euler定理等等)及它们的推广;PetrMDouglasMNeumann定理(包括Napoleon定理及其推广等);几何不等式;正多边形及某些非初等几何作图等。另外,书中还提出一些未解决问题。

对于关心初等几何定理的机器证明的读者,本书是一本内容丰富的有意义的读物,它也可供有关科研人员参考。

朱尧辰,研究员

(中国科学院应用数学研究所)

Zhu Yaochen, Professor

(Institute of Applied Mathematics,CAS)