群論問題的形式化及驗(yàn)證研究.pdf

1、本文以一種典型的形式化方法——邏輯化方法為研究方向，研究如何應(yīng)用計(jì)算機(jī)程序證明數(shù)學(xué)定理。具體地說，如何通過一套邏輯符號體系將人腦的推理證明過程形式化，從而轉(zhuǎn)化為一系列可在計(jì)算機(jī)上自動實(shí)現(xiàn)的推理證明過程。
　　采用形式語言(邏輯語言)表示數(shù)學(xué)定理、證明過程是定理證明器的一個重要任務(wù)，使得數(shù)學(xué)定理的表述以及定理證明過程的每個步驟能夠被計(jì)算機(jī)程序驗(yàn)證。我們必須使用嚴(yán)格的語法規(guī)則和具有明確語義的形式語言表達(dá)數(shù)學(xué)對象，包括定義、命題和證明。

2、
　　本文主要采用一階邏輯語言對數(shù)學(xué)中的群論領(lǐng)域進(jìn)行形式化研究，并使用定理證明系統(tǒng)Prover9進(jìn)行形式化驗(yàn)證，主要取得了如下成果:
　　1、基于形式化方法的兩個方面——形式化描述與形式化驗(yàn)證，給出了群論相關(guān)知識的形式化過程的基本步驟。
　　2、基于TPTP中群論領(lǐng)域一些已經(jīng)被形式化的結(jié)論，給出了群運(yùn)算封閉性、恒等元、逆元、結(jié)合律、消去律、交換律、恒等元的唯一性、逆元的唯一性、滿足一定條件的集合的形式化描述方法。從而完