基于Alloy的两个群定义的等价性验证  

Automated Verification of Equivalence of Two Group Definitions Based on Alloy

作　　者：邹科 江建国[1] 徐月 张新钢 

机构地区：[1]辽宁师范大学数学学院,辽宁大连 [2]大连市第二十四中学,辽宁大连

出　　处：《应用数学进展》2017年第9期1050-1055,共6页Advances in Applied Mathematics

摘　　要：群论是代数系统中的重要组成部分。本文提出一种使用Alloy验证群论中定理的新方法。使用Alloy对群的两种定义进行了形式化描述,并通过Alloy分析器实现了对这两种群定义的自动化验证。实验结果表明,该方法可行并且具有较高的效率。Group theory is an important part of algebraic system. This paper presents a new method to verify two Group definitions using Alloy. The two definitions of Group are formally described using Alloy, and the automatic verification of the two definitions of Group is realized by the Alloy analyzer. The experimental results show that the method is feasible and has high efficient.

关 键 词：群论 ALLOY 形式化描述 自动化验证 

分 类 号：TP39[自动化与计算机技术—计算机应用技术]