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

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

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

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

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

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