目錄
第1章 Desargues幾何與Desargues數(shù)系 1
1.1 常用幾何的Hilbert公理系統(tǒng) 1
1.2 無限公理與Desargues公理 5
1.3 Desargues平面中的有理點 11
1.4 Desargues數(shù)系與有理數(shù)子系 16
1.5 直線上的Desargues數(shù)系 21
1.6 Desargues平面的附屬Desargues數(shù)系 26
1.7 Desargues平面幾何的坐標(biāo)系 38
第2章 垂直幾何、度量幾何與常用幾何 45
2.1 Pascal公理與乘法交換公理——(無序)Pascal幾何 45
2.2 垂直公理與（無序）垂直幾何 52
2.3 （無序）垂直幾何的垂直坐標(biāo) 61
2.4 （無序）度量幾何 71
2.5 次序公理與有序度量幾何 80
2.6 常用幾何及其關(guān)屬幾何 86
第3章 幾何定理證明的機械化與Hilbert機械化定理 90
3.1 歐幾里得證明方法小議 90
3.2 幾何概念坐標(biāo)表示的標(biāo)準(zhǔn)化 93
3.3 定理證明的機械化與Hilbert關(guān)于Pascal幾何中交點定理的機械化定理 97
3.4 Hilbert機械化證法舉例 100
3.5 Hilbert機械化定理的證明 110
第4章 （常用）無序幾何的機械化定理 117
4.1 概述 117
4.2 多項式的因子分解 119
4.3 多項式組的整序 125
4.4 代數(shù)簇的構(gòu)造性理論——不可約升列與不可約代數(shù)簇 133
4.5 代數(shù)簇的構(gòu)造性理論——代數(shù)簇的不可約分解 141
4.6 代數(shù)簇的構(gòu)造性理論——維數(shù)概念與維數(shù)定理 146
4.7 無序幾何機械化定理的證明 149
4.8 無序幾何機械化證法舉例 156
第5章 （常用）有序幾何的機械化定理 171
5.l 有序幾何定理證明機械化概述 171
5.2 Tarski定理與Seidenberg方法 177
5.3 有序幾何定理機械化證法舉例 184
第6章 各種幾何的機械化定理 190
6.1 概述 190
6.2 投影幾何定理證明的機械化 191
6.3 Bolyai-Lobachevsky雙曲型非歐幾何定理證明的機械化 l99
6.4 Riemann橢圓型非歐幾何定理證明的機械化 212
6.5 兩種圓幾何學(xué)定理證明的機械化 217
6.6 超越函數(shù)公式證明的機械化 219
參考文獻 231