數(shù)學(xué)機械化思想的歷史發(fā)展.pdf

1、在已有工作的基礎(chǔ)上，本文從總體的和全面的角度著眼，從數(shù)學(xué)機械化思想發(fā)展的關(guān)鍵人物和關(guān)鍵事件入手，結(jié)合對重點案例的分析，綜合考察了數(shù)學(xué)機械化思想發(fā)展的歷史過程，特別是揭示數(shù)學(xué)機械化思想的產(chǎn)生和發(fā)展。 已有研究工作對數(shù)學(xué)機械化的思想發(fā)展雖有認識，但系統(tǒng)、全面地揭示其發(fā)展脈絡(luò)仍是數(shù)學(xué)史研究地重要課題。本文從笛卡爾、萊布尼茨關(guān)于機械代替人腦處理數(shù)學(xué)設(shè)想出發(fā)，進一步揭示了希爾伯特的數(shù)學(xué)機械化方法，塔斯基、王浩的創(chuàng)造性工作，以及吳文俊的卓越

2、貢獻，為更深刻地理解數(shù)學(xué)機械化思想提供了有力的支撐。 國內(nèi)的數(shù)學(xué)機械化研究一直關(guān)注吳文俊院士的已有成果，對西方學(xué)者的研究方法和思路介紹不多。本文在研讀西方文獻的基礎(chǔ)上，比較詳細地介紹了數(shù)學(xué)機械化研究在西方的發(fā)展，特別突出了西方學(xué)者對于數(shù)學(xué)機械化的不同理解和研究取向。 本文的重點在于介紹塔斯基和王浩在數(shù)學(xué)機械化研究中的貢獻。塔斯基首先在理論上證明：初等幾何和代數(shù)范圍的命題都可以通過機械方法判定。塔斯基得出的結(jié)論給定理判定問

3、題的研究帶來了曙光，雖然哥德爾不完備定理否定了希爾伯特的思路，但是在其它方向?qū)ふ遗卸ǚ椒ㄊ强尚械摹?電子計算機的誕生為數(shù)學(xué)機械化做好了物質(zhì)條件上的準備。1959年，華裔邏輯學(xué)家王浩在IBM 704型計算機上編制的程序高效地證明了《數(shù)學(xué)原理》中的220條定理，正是王浩吹響了向數(shù)學(xué)機械化邁進的號角。王浩強調(diào)算法的重要性，合理的算法可以最大限度的發(fā)揮使計算機的效力。王浩提出，計算與證明存在不同之處，將證明轉(zhuǎn)化為計算是實現(xiàn)數(shù)學(xué)問題機器證

4、明的根本途徑；應(yīng)當(dāng)注意通常的多項式復(fù)雜類，并認為這是有可能取得突破的方向。 王浩的思想無疑是正確的。吳文俊數(shù)學(xué)機械化方法的成功正是由于找到了處理多項式復(fù)雜關(guān)系的有力工具。更為可喜的是，吳文俊的數(shù)學(xué)機械化方法是在不了解西方學(xué)者研究的情況下獨立取得的，而促成這一突破性成果的主要思想竟然來自中國古代的數(shù)學(xué)家。蘊含于中國傳統(tǒng)數(shù)學(xué)中的方程解法和算法化思想在數(shù)學(xué)機械化的研究中大放異彩，揭示了具有機械化特征的中國傳統(tǒng)數(shù)學(xué)思想的強大生命力。

5、 數(shù)學(xué)機械化的思想源自西方，但是高效、廣泛的定理機械化證明方法的得出，卻得益于具有機械化特征的中國傳統(tǒng)數(shù)學(xué)思想的啟發(fā)。對數(shù)學(xué)機械化思想發(fā)展的歷史研究充分說明，中國傳統(tǒng)數(shù)學(xué)思想對于數(shù)學(xué)發(fā)展有其獨特貢獻，機械化的數(shù)學(xué)與電子計算機的緊密結(jié)合，必將深刻改變?nèi)藗冄芯繑?shù)學(xué)的方式，必將從根本上影響數(shù)學(xué)的發(fā)展。 本文在附錄中給出了C語言描述的“增乘開放法”，以及運用數(shù)學(xué)機械化自動推理平臺( MMP )實現(xiàn)定理證明的實例。 通過對數(shù)學(xué)