基于Alloy的两个群定义的等价性验证
Automated Verification of Equivalence of Two Group Definitions Based on Alloy
DOI: 10.12677/AAM.2017.69127, PDF,   
作者: 邹 科, 江建国, 徐 月：辽宁师范大学数学学院，辽宁 大连；张新钢：大连市第二十四中学，辽宁 大连
关键词: 群论；Alloy；形式化描述；自动化验证；Group Theory； Alloy； Formal Description； Automated Verification
摘要: 群论是代数系统中的重要组成部分。本文提出一种使用Alloy验证群论中定理的新方法。使用Alloy对群的两种定义进行了形式化描述，并通过Alloy分析器实现了对这两种群定义的自动化验证。实验结果表明，该方法可行并且具有较高的效率。
Abstract: 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的两个群定义的等价性验证[J]. 应用数学进展, 2017, 6(9): 1050-1055. https://doi.org/10.12677/AAM.2017.69127

参考文献

[1] 张禾瑞. 近世代数基础[M]. 北京: 高等教育出版社, 2008.
[2] Slaney, J. (1993) FINDER: Finite Domain Enu-merator. Version 3.0 Notes and Guide. Australian National University, Canberra.
[3] Zhang, J. (1996) Constructing Finite Algebras with Falcon. Journal of Automated Reasoning, 16, 1-22.
[Google Scholar] [CrossRef] 
[4] Zhang, H.T. and Stickel, M. (1994) Implementing the Davis-Putnam Algorithm by Tries. Technical Report, University of Iowa, Iowa City.
[5] McCune, W. (1994) A Davis-Putnam Pro-gram and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Mathematics and Com-puter Science Division, Argonne National Laboratory, Argonne.
[6] Zhang, J. and Zhang, H.T. (1995) SEM: A System for Enumerating Models. In: Department of Philosophy University of Wisconsin-Madison Mathematics and Computer Science, 298-303.
[7] Torlak, E. and Jackson, D. (2007) Kodkod: A Relational Model Finder. Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Braga, 632-647.
[Google Scholar] [CrossRef] 
[8] Jackson, D. (2006) Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, MA.
[9] Jackson, D. (n.d.) Alloy: A Language & Tool for Relational Models. http://alloy.mit.edu/alloy
[10] Jackson, D. (2000) Automating First-Order Relational Logic. ACM SIGSOFT Software Engineering Notes, 25, 130-139.
[Google Scholar] [CrossRef] 
[11] Clarke, E.M. and Emerson, E.A. (1981) Design and Synthesis of Synchronization Skeletons Using Branching-time Temporal Logic. In: Logic of Pro-grams, Lecture Notes in Computer Science, Springer, 133: 52-71.
[12] Torlak, E. and Dennis, G. (2006) Kodkod for Alloy Users. Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory, Cam-bridge.
[13] 聂灵沼, 丁石孙. 代数学引论[M]. 北京: 高等教育出版社, 2011: 23-25.
[14] 杨家海, 姜宁, 安长青, 李福亮. 基于形式化描述的交换机网络自动配置策略的设计与实现[J]. 清华大学学报(自然科学版), 2012(8): 1041-1048.

为你推荐