本文關(guān)鍵詞：群論問(wèn)題的形式化及驗(yàn)證研究　出處：《西南交通大學(xué)》2017年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 形式化方法 一階邏輯語(yǔ)言 形式化描述 形式化驗(yàn)證 群論

【摘要】：本文以一種典型的形式化方法——邏輯化方法為研究方向,研究如何應(yīng)用計(jì)算機(jī)程序證明數(shù)學(xué)定理。具體地說(shuō),如何通過(guò)一套邏輯符號(hào)體系將人腦的推理證明過(guò)程形式化,從而轉(zhuǎn)化為一系列可在計(jì)算機(jī)上自動(dòng)實(shí)現(xiàn)的推理證明過(guò)程。采用形式語(yǔ)言(邏輯語(yǔ)言)表示數(shù)學(xué)定理、證明過(guò)程是定理證明器的一個(gè)重要任務(wù),使得數(shù)學(xué)定理的表述以及定理證明過(guò)程的每個(gè)步驟能夠被計(jì)算機(jī)程序驗(yàn)證。我們必須使用嚴(yán)格的語(yǔ)法規(guī)則和具有明確語(yǔ)義的形式語(yǔ)言表達(dá)數(shù)學(xué)對(duì)象,包括定義、命題和證明。本文主要采用一階邏輯語(yǔ)言對(duì)數(shù)學(xué)中的群論領(lǐng)域進(jìn)行形式化研究,并使用定理證明系統(tǒng)Prｏｖer9進(jìn)行形式化驗(yàn)證,主要取得了如下成果:1、基于形式化方法的兩個(gè)方面——形式化描述與形式化驗(yàn)證,給出了群論相關(guān)知識(shí)的形式化過(guò)程的基本步驟。2、基于TPTP中群論領(lǐng)域一些已經(jīng)被形式化的結(jié)論,給出了群運(yùn)算封閉性、恒等元、逆元、結(jié)合律、消去律、交換律、恒等元的唯一性、逆元的唯一性、滿足一定條件的集合的形式化描述方法。從而完成了群論中一些TPTP中缺少的知識(shí)的形式化描述,即阿貝爾群、正規(guī)子群、正規(guī)化子、中心化子等。然后形式化描述了一些相關(guān)的命題及定理,并通過(guò)定理證明工具Prｏｖer9驗(yàn)證了其形式化描述的正確性。3、選擇了群論中的一個(gè)開問(wèn)題,對(duì)其形式化描述并求解,根據(jù)本文使用的形式化方法,為此開問(wèn)題的解決做了推進(jìn)。
【學(xué)位授予單位】：西南交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：O152

【參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前6條

1 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

2 王敏;;數(shù)理邏輯中的命題符號(hào)化的幾個(gè)值得注意的問(wèn)題[J];科技信息;2010年09期

3 王靜;;離散數(shù)學(xué)教學(xué)中關(guān)于命題符號(hào)化問(wèn)題的討論[J];科技信息(科學(xué)教研);2008年25期

4 何鋒;;離散數(shù)學(xué)教學(xué)中的命題符號(hào)化難點(diǎn)討論[J];計(jì)算機(jī)教育;2007年17期

5 周宏斌,黃連生,桑田;基于串空間的安全協(xié)議形式化驗(yàn)證模型及算法[J];計(jì)算機(jī)研究與發(fā)展;2003年02期

6 閆安,唐稚松;在 XYZ/ E中實(shí)現(xiàn)混成實(shí)時(shí)系統(tǒng)——蒸氣鍋爐控制問(wèn)題的解決(英文)[J];軟件學(xué)報(bào);2000年06期

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前3條

1 王建林;基于Isabelle平臺(tái)的一般拓?fù)鋵W(xué)機(jī)械化及自動(dòng)定理證明研究[D];華東師范大學(xué);2012年

2 沈勝宇;模型檢驗(yàn)的反例解釋[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

3 王海霞;運(yùn)算電路的形式化驗(yàn)證方法研究[D];中國(guó)科學(xué)院研究生院（計(jì)算技術(shù)研究所）;2004年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前2條

1 李黎明;代數(shù)系統(tǒng)和復(fù)數(shù)理論的形式化及DS編碼器的驗(yàn)證應(yīng)用[D];首都師范大學(xué);2012年

2 劉素姣;一階謂詞邏輯在人工智能中的應(yīng)用[D];河南大學(xué);2004年

，

本文編號(hào)：1309106