基于Alloy的群论定理的机器验证
发布时间：2020-10-26 23:11
群论定理的机器验证是自动推理领域内的一个研究课题,其验证程序广泛应用于代数学、密码学、计算机科学等学科中。早期开发的验证程序都属于原型程序,在验证群论定理时有一定的缺陷和不足,到目前为止都没有了后续的改进工作。这些验证程序应用的描述语言表达能力十分有限,无法描述较复杂的群论定理。另外,它们验证时运行的效率相对较低,只能处理部分的群论问题。本文提出一种基于Alloy分析器验证群论定理的新方法。该方法首先通过Alloy语言对群论定理进行建模,然后使用Alloy分析器对建立的模型自动验证。使用本文提出的新方法验证群论定理有以下优点:1.Alloy建模语言的表达能力非常强,能够简洁的描述群论定理中的各种关系;2.Alloy分析器具有破除对称性的高效算法,可以显著提高验证群论定理的效率;3.Alloy分析器能够将最终的结果以图形的形式显示出来,可读性非常强。基于提出的新方法,本文利用Alloy对群论中的部分定义和定理进行了机器验证实验。实验结果表明,利用Alloy验证群论定理相对更简洁、更高效,而且得到的结果更直观。最后,希望Alloy可以成为验证群论定理的一个有力工具,并能够对以后研究群论中的开问题或猜想有所帮助。
【学位单位】：辽宁师范大学
【学位级别】：硕士
【学位年份】：2018
【中图分类】：O152
【部分图文】：
辽宁师范大学硕士学位论文 群论定理的验证1 验证平台及验证数据本章节中使用 Alloy 分析器对群论定理的模型进行检测实验。实验运行的计算机具体如下：Windows 7 操作系统，Intel(R) Core(TM) i5-2450M CPU，2.5GHz，4.0M。Alloy 分析器主要提供三种类型的 SAT 求解器，如 Zchaff 求解器、SAT4J 求解器inisat 求解器。针对本文中部分定理的 Alloy 模型，分别使用三种求解器进行自动分测，得到的运行时间数据如下图：
图 4.2 生成含有三个元素群的操作界面Fig.4.2 Operation Interface with Three Elements Group左侧为 Alloy 语言描述的语句，右侧为验证后的结果。基于 Alloy 语言建立群的时，使用的是谓词 predicate 语句，对应的执行命令为 run 语句。语句中的 3 表示在范围内查找，1 表示在一个群G 中。其结果能够显示使用的求解器类型以及运行时间句“Instance found”表示找到实例模型。点击结果中“Instance”，将会得到由 Al析器提供的可视化结果，如下图：
图 4.3 含有三个元素群的实例模型Fig.4.3 Instance Model with Three Elements Group其中 Group 代表生成的群，Element0，Element1，Element2 是 Group 中的三个元果中可以显示以下信息：(1) Element2 是该群中的单位元，并与自己互为逆元；(2) Element0 和 Element1 互为逆元；(3) 元素经过二元运算后对应的元。经过二元运算后得到的元素间关系如下表所示：表 4.1 模型中元素间的二元运算Tab.4.1 Binary Operation between Elements in Model元素名称 Element0 Element1 Element2Element0 Element1 Element2 Element0Element1 Element2 Element0 Element1Element2 Element0 Element1 Element2
【参考文献】
本文编号：2857656
【学位单位】：辽宁师范大学
【学位级别】：硕士
【学位年份】：2018
【中图分类】：O152
【部分图文】：
辽宁师范大学硕士学位论文 群论定理的验证1 验证平台及验证数据本章节中使用 Alloy 分析器对群论定理的模型进行检测实验。实验运行的计算机具体如下：Windows 7 操作系统，Intel(R) Core(TM) i5-2450M CPU，2.5GHz，4.0M。Alloy 分析器主要提供三种类型的 SAT 求解器，如 Zchaff 求解器、SAT4J 求解器inisat 求解器。针对本文中部分定理的 Alloy 模型，分别使用三种求解器进行自动分测，得到的运行时间数据如下图：
图 4.2 生成含有三个元素群的操作界面Fig.4.2 Operation Interface with Three Elements Group左侧为 Alloy 语言描述的语句，右侧为验证后的结果。基于 Alloy 语言建立群的时，使用的是谓词 predicate 语句，对应的执行命令为 run 语句。语句中的 3 表示在范围内查找，1 表示在一个群G 中。其结果能够显示使用的求解器类型以及运行时间句“Instance found”表示找到实例模型。点击结果中“Instance”，将会得到由 Al析器提供的可视化结果，如下图：
图 4.3 含有三个元素群的实例模型Fig.4.3 Instance Model with Three Elements Group其中 Group 代表生成的群，Element0，Element1，Element2 是 Group 中的三个元果中可以显示以下信息：(1) Element2 是该群中的单位元，并与自己互为逆元；(2) Element0 和 Element1 互为逆元；(3) 元素经过二元运算后对应的元。经过二元运算后得到的元素间关系如下表所示：表 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 杨家海;姜宁;安常青;李福亮;;基于形式化描述的交换机网络自动配置策略的设计与实现[J];清华大学学报(自然科学版);2012年08期
2 张景中;彭翕成;;自动推理及其在数学教育中的应用[J];数学教育学报;2008年04期
相关博士学位论文 前1条
1 王海霞;运算电路的形式化验证方法研究[D];中国科学院研究生院（计算技术研究所）;2004年
相关硕士学位论文 前2条
1 李婉;群论问题的形式化及验证研究[D];西南交通大学;2017年
2 毛丹雯;线性空间理论在定理证明器HOL中的形式化[D];北京化工大学;2013年
本文编号：2857656
本文链接：https://www.wllwen.com/kejilunwen/yysx/2857656.html
