機 器 證 明 

1. Descarstes幾何命題代數化
2. Leibnitz的Universal language
3. D.Hilbert機械化定理
4. Tarski 1931年,1950年
5. Godel不完備定理1931年
6. 王浩1959年
7. 吳文俊1977年STAR
8. 張景中,周咸青,高小山 :非平凡幾何定理的可讀性定理-----由面積法+消點法得到的演算法

1. 幾何基礎-----------------D.Hilbert
2. 解題研究p.209------------張景中
3. 數學傳播季刊15卷4期
4. 機械化證明的新曙光-------科學月刊1997/12
5. 傳播季刊11卷4期----------王浩,吳文俊機器證明與發明
6. 笛卡爾之夢
7. 九章出版社---------------張景中先生主持策劃的超級畫板問世