幾何定理機器證明的幾何不變量方法

第1章幾何定理機器證明概述
1.1模擬人的思維——人工智能的開始
1.2 Gelernter的幾何定理證明機
1.3幾何定理機器證明的吳方法
1.4幾何定理自動發現的吳方法
第1章小結
第2章面積法
2.1傳統的證明方法和機器證明的比較
2.2有向三角形的帶號面積
2.2.1公理
2.2.2基本命題
2.3 Hilbert交點命題
2.3.1命題的描述
2.3.2幾何命題的謂詞形式
2.4面積法
2.4.1從面積中消去點
2.4.2從比例中消去點
2.4.3 自由點和面積坐標
2.4.4幾何定理證明舉例
2.4.5其他的消元技術
2.5面積法和仿射幾何
2.5.1平面仿射幾何
2.5.2面積法和仿射幾何
2.6應用
2.6.1公式推導
2.6.2 n3構型的存在性
2.6.3 Ceva與Menelus定理的推廣
第2章小結
第3章平面幾何機器證明
3.1勾股差
3.1.1勾股差和垂直
3.1.2勾股差和平行
3.1.3勾股差和面積
3.2構造型幾何命題
3.2.1線性構造型幾何命題
3.2.2最小構造集合
3.2.3謂詞形式
3.3線性可構型幾何命題的機器證明
3.3.1算法
3.3.2優化的消去技巧
3.4比率構造
3.4.1更多的比率構造
3.4.2全角法的機械化
3.5面積坐標
3.5.1面積坐標系
3.5.2面積坐標和三角形的特殊點
3.6三角函數和共圓點
3.6.1共圓定理
3.6.2共圓點的消去
3.7可構型幾何命題的機器證明
3.7.1從幾何量中消點
3.7.2偽除法和三角形式
3.7.3可構型幾何命題的機器證明
3.8基於演繹數據庫的全角方法
3.8.1建立幾何信息庫
3.8.2基於幾何信息庫的機器證明
第3章小結
第4章演繹數據庫方法
4.1結構化的演繹數據庫和推理策略
4.1.1基於結構化數據的推理
4.1.2有關的工作
4.2幾何推理規則
4.2.1 幾何推理規則
4.2.2非退化條件
4.2.3准確的數值圖形的構造
4.3結構化數據庫
4.3.1數據庫的結構
4.3.2證明的生成
4.4搜索和控制的策略
4.4.1基於數據的搜索
4.4.2避免冗余推理
4.5構造輔助點和Skolem化
4.6算法的實現與例題
4.6.1算法的實現
4.6.2應用
4.6.3測試結果和例子
附錄
第4章小結
第5章 立體幾何中的定理自動證明
5.1帶號體積
5.1.1共面定理
5.1.2體積和平行
5.1.3體積與三維仿射幾何
5.2構造型幾何命題
5.2.1構造型幾何命題
5.2.2構造型幾何圖形
5.3線性構造型幾何命題的機器證明
5.3.1關於體積的消點法
5.3.2由面積比中消點
5.3.3 由長度比中消點
5.3.4 自由點和體積坐標
5.3 5例子
5.4空問中的勾股差
5.4.1勾股差與垂直
5.4.2勾股差與體積
5.5體積法
5.5.1算法
5.5.2例子
5.6體積坐標系
第5章小結
第6章 非歐幾何定理的機器證明
6.1 Cayley—Klein九種平面幾何
6.1.1直線上的三種度量
6.1.2角度的三種度量
6.1.3九種平面幾何
6.2 Cayley—Klein幾何的轉化定理
6.3雙曲幾何面積法
6.4雙曲幾何的消元法
6.4.1基本幾何命題
6.4.2從比率中消去點
6.4.3從線性的幾何量中消去點
6.4.4從二次幾何量中消去點
6.4.5消去自由點
6.4.6消去共圓的點
6.5算法的實現與例子
第6章小結
第7章 向量和機器證明
7.1三維度量空問幾何
7.1.1 內積和度量向量空間
7.1.2度量向量空間的外積
7.2立體度量幾何
7.2.1內積和外積
7.2.2構造型幾何語句
7.3基於向量計算的機器證明
7.3.1向量消點法
7.3.2從內積和外積中消點
7.3.3算法
7.4度量平面幾何中的機器證明
7.4.1歐氏平面幾何的向量方法
7.4.2 Minkowsky平面幾何中的機器證明
7.5使用復數的機器證明
第7章小結
參考文獻
索引