Pavel Pech University of South Bohemia,
Czech Republic
Selected Topics in Geometry
With Classical VS.
Computer Proving
2007, 239pp.
Hardcover
ISBN 9789812709424
P.沛赫著
數(shù)學(xué)機(jī)器證明是上世紀(jì)70年代以來發(fā)展起來的一個(gè)重要的數(shù)學(xué)研究領(lǐng)域。本書是捷克數(shù)學(xué)家所寫的一本關(guān)于初等幾何定理的機(jī)器證明的專著。作者基于Gr?bner基消元理論給出一些著名的初等幾何定理和公式的自動(dòng)證明技術(shù),并應(yīng)用這些方法發(fā)現(xiàn)一些新公式,解決一些幾何不等式,完成某些用通常尺規(guī)作圖不易作出的幾何作圖。特別是,對(duì)于每個(gè)問題,作者首先給出自動(dòng)證明方法,然后給出經(jīng)典方法(盡可能不使用計(jì)算機(jī))讓讀者比較兩種方法的優(yōu)缺點(diǎn),從而進(jìn)一步理解機(jī)器證明的基本思想和技術(shù)。
全書含9章。1.引論,概述了機(jī)器證明的意義、思想和歷史;2.定理自動(dòng)證明,給出本書的理論基礎(chǔ),主要是代數(shù)幾何的一些基本概念和結(jié)果,以及自動(dòng)推導(dǎo)和自動(dòng)發(fā)現(xiàn)的基本原理;3-9.對(duì)于某些精心選擇的重要的著名的初等幾何定理和公式逐一給出自動(dòng)證明和經(jīng)典證明,并加以評(píng)注,其中包括:三解形和四邊形的面積公式(Heron公式和Staudt公式)及它們的推廣;SimsonMWallece三垂足共線定理及推廣;多邊形的橫截定理(Ceva定理、Menelaus定理、Euler定理等等)及它們的推廣;PetrMDouglasMNeumann定理(包括Napoleon定理及其推廣等);幾何不等式;正多邊形及某些非初等幾何作圖等。另外,書中還提出一些未解決問題。
對(duì)于關(guān)心初等幾何定理的機(jī)器證明的讀者,本書是一本內(nèi)容豐富的有意義的讀物,它也可供有關(guān)科研人員參考。
朱堯辰,研究員
(中國科學(xué)院應(yīng)用數(shù)學(xué)研究所)
Zhu Yaochen, Professor
(Institute of Applied Mathematics,CAS)