群論定理的機(jī)器驗證是自動推理領(lǐng)域內(nèi)的一個研究課題,其驗證程序廣泛應(yīng)用于代數(shù)學(xué)、密碼學(xué)、計算機(jī)科學(xué)等學(xué)科中。早期開發(fā)的驗證程序都屬于原型程序,在驗證群論定理時有一定的缺陷和不足,到目前為止都沒有了后續(xù)的改進(jìn)工作。這些驗證程序應(yīng)用的描述語言表達(dá)能力十分有限,無法描述較復(fù)雜的群論定理。另外,它們驗證時運(yùn)行的效率相對較低,只能處理部分的群論問題。本文提出一種基于Alloy分析器驗證群論定理的新方法。該方法首先通過Alloy語言對群論定理進(jìn)行建模,然后使用Alloy分析器對建立的模型自動驗證。使用本文提出的新方法驗證群論定理有以下優(yōu)點(diǎn):1.Alloy建模語言的表達(dá)能力非常強(qiáng),能夠簡潔的描述群論定理中的各種關(guān)系;2.Alloy分析器具有破除對稱性的高效算法,可以顯著提高驗證群論定理的效率;3.Alloy分析器能夠?qū)⒆罱K的結(jié)果以圖形的形式顯示出來,可讀性非常強(qiáng)。基于提出的新方法,本文利用Alloy對群論中的部分定義和定理進(jìn)行了機(jī)器驗證實驗。實驗結(jié)果表明,利用Alloy驗證群論定理相對更簡潔、更高效,而且得到的結(jié)果更直觀。最后,希望Alloy可以成為驗證群論定理的一個有力工具,并能夠?qū)σ院笱芯咳赫撝械拈_問題或猜想有所幫助。
【學(xué)位單位】：遼寧師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位年份】：2018
【中圖分類】：O152
【部分圖文】：

遼寧師范大學(xué)碩士學(xué)位論文 群論定理的驗證1 驗證平臺及驗證數(shù)據(jù)本章節(jié)中使用 Alloy 分析器對群論定理的模型進(jìn)行檢測實驗。實驗運(yùn)行的計算機(jī)具體如下：Windows 7 操作系統(tǒng)，Intel(R) Core(TM) i5-2450M CPU，2.5GHz，4.0M。Alloy 分析器主要提供三種類型的 SAT 求解器，如 Zchaff 求解器、SAT4J 求解器inisat 求解器。針對本文中部分定理的 Alloy 模型，分別使用三種求解器進(jìn)行自動分測，得到的運(yùn)行時間數(shù)據(jù)如下圖：

圖 4.2 生成含有三個元素群的操作界面Fig.4.2 Operation Interface with Three Elements Group左側(cè)為 Alloy 語言描述的語句，右側(cè)為驗證后的結(jié)果�；� Alloy 語言建立群的時，使用的是謂詞 predicate 語句，對應(yīng)的執(zhí)行命令為 run 語句。語句中的 3 表示在范圍內(nèi)查找，1 表示在一個群G 中。其結(jié)果能夠顯示使用的求解器類型以及運(yùn)行時間句“Instance found”表示找到實例模型。點(diǎn)擊結(jié)果中“Instance”，將會得到由 Al析器提供的可視化結(jié)果，如下圖：

圖 4.3 含有三個元素群的實例模型Fig.4.3 Instance Model with Three Elements Group其中 Group 代表生成的群，Element0，Element1，Element2 是 Group 中的三個元果中可以顯示以下信息：(1) Element2 是該群中的單位元，并與自己互為逆元；(2) Element0 和 Element1 互為逆元；(3) 元素經(jīng)過二元運(yùn)算后對應(yīng)的元。經(jīng)過二元運(yùn)算后得到的元素間關(guān)系如下表所示：表 4.1 模型中元素間的二元運(yùn)算Tab.4.1 Binary Operation between Elements in Model元素名稱 Element0 Element1 Element2Element0 Element1 Element2 Element0Element1 Element2 Element0 Element1Element2 Element0 Element1 Element2
【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 楊家海;姜寧;安常青;李福亮;;基于形式化描述的交換機(jī)網(wǎng)絡(luò)自動配置策略的設(shè)計與實現(xiàn)[J];清華大學(xué)學(xué)報(自然科學(xué)版);2012年08期

2 張景中;彭翕成;;自動推理及其在數(shù)學(xué)教育中的應(yīng)用[J];數(shù)學(xué)教育學(xué)報;2008年04期

相關(guān)博士學(xué)位論文 前1條

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

相關(guān)碩士學(xué)位論文 前2條

1 李婉;群論問題的形式化及驗證研究[D];西南交通大學(xué);2017年

2 毛丹雯;線性空間理論在定理證明器HOL中的形式化[D];北京化工大學(xué);2013年

本文編號：2857656