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

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

圖 4.2 生成含有三個元素群的操作界面Fig.4.2 Operation Interface with Three Elements Group左側(cè)為 Alloy 語言描述的語句，右側(cè)為驗證后的結(jié)果。基于 Alloy 語言建立群的時，使用的是謂詞 predicate 語句，對應的執(zhí)行命令為 run 語句。語句中的 3 表示在范圍內(nèi)查找，1 表示在一個群G 中。其結(jié)果能夠顯示使用的求解器類型以及運行時間句“Instance found”表示找到實例模型。點擊結(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)過二元運算后對應的元。經(jīng)過二元運算后得到的元素間關系如下表所示：表 4.1 模型中元素間的二元運算Tab.4.1 Binary Operation between Elements in Model元素名稱 Element0 Element1 Element2Element0 Element1 Element2 Element0Element1 Element2 Element0 Element1Element2 Element0 Element1 Element2
【參考文獻】

相關期刊論文 前2條

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

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

相關博士學位論文 前1條

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

相關碩士學位論文 前2條

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

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

本文編號：2857656