基于Alloy的73构形存在性定理的机器验证
Machine Verification of the Existence Theorem of Configuration 73 Based on Alloy
DOI: 10.12677/AAM.2017.68123, PDF, HTML, XML, 下载: 1,492  浏览: 1,754 
作者: 徐 月, 江建国, 邹 科：辽宁师范大学数学学院，辽宁 大连；张新钢：大连市第二十四中学，辽宁 大连
关键词: 73构形；有限几何；Alloy分析器；机器验证；Configuration 73； Finite Geometry； Alloy； Machine Verification
摘要: 73构形的存在性是有限几何中的一个基本问题。本文给出了一种用Alloy分析器自动验证73构形的存在性的方法。该方法使用 Alloy语言对Fano提出的公理系统和需要验证的定理进行形式化，然后利用Alloy分析器分析定理是否满足属性要求。实验结果表明本文提出的机器验证方法是可行的。
Abstract: The existence of the configuration 73 is a basic problem in finite geometry. This paper presents a method for automatically verifying the existence of configuration 73 using an Alloy analyzer. This method uses Alloy language to formalize Fano’s axiom system and the need to validate the theorem, and then uses the Alloy analyzer to analyze whether the theorem satisfies the attribute re-quirement. It is shown that the proposed method of verification is feasible.
文章引用：徐月, 江建国, 邹科, 张新钢. 基于Alloy的73构形存在性定理的机器验证[J]. 应用数学进展, 2017, 6(8): 1027-1033. https://doi.org/10.12677/AAM.2017.68123

参考文献

[1] Gropp, H. (2004) Configuration between Geometry and Combinatorics. Discrete Applied Mathematics, 138, 79-88.
https://doi.org/10.1016/S0166-218X(03)00271-3
[2] Sturmfels, B. (1991) Computational Algebraic Geometry of Projective Configuration. Journal of Symbolic Computation, 11, 595-618.
https://doi.org/10.1016/S0747-7171(08)80121-6
[3] van Straten, M.P. (1948) The Topology of the Configura-tions of Desargues and Pappus. Rep. Math. Colloquium, 3-17.
[4] Gropp, H. (1990) On the History of Configuration. In: Diez, A., Ed., Internet, Symposium on Structures in Math, Theories, Bilbao, 263-268.
[5] Gropp, H. (1994) On Symmetric Spatil Configurations. Discrete Mathematics, 125, 201-209.
https://doi.org/10.1016/0012-365X(94)90161-9
[6] Kantor, S. (1881) Die Configurationen (3,3)10. Sitzungsber Akad Wiss Wien Math Natural Kl, 84, 1291-1314.
[7] Fano, G. (1892) Sui Postulate Fondamentali Della Geometria Proiettiva. Giornale di Matematiche, 30, 106-132.
[8] Coxeter, H.M. (1983) My Graph. Proceedings of the London Mathematical Society, s3-46, 117-136.
https://doi.org/10.1112/plms/s3-46.1.117
[9] Grünbaum, B. and Rigby, J.F. (1990) The Real Configuration (214). Journal of London Mathematical Society, 41, 336-346.
https://doi.org/10.1112/jlms/s2-41.2.336
[10] Grünbaum, B. (2006) Configurations of Points and Lines. Davis, C. and Ellers, W.W., Eds., American Mathematical Society, Rhode Island, 179-225.
[11] Jackson, D. (2000) Automating First-Order Relational Logic. ACM SIGSOFT Software Engineering Notes, 25, 130-139.
https://doi.org/10.1145/357474.355063
[12] Jackson, D. (2006) Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge.
[13] Jackson, D. (2002) Alloy: A Language & Tool For Relational Models. http://alloy.mit.edu/alloy
[14] Khurshid, S. and Marinov, D. (2004) TestEra: Specification-Based Testing of Java Problems Using SAT. Automated Software Engineering, 11, 403-434.
https://doi.org/10.1023/B:AUSE.0000038938.10589.b9
[15] Narain, S. (2004) Network Configuration Manage-ment Via Model Finding. Conference on Large Installation System Administration Conference, 2, 15.
[16] Andoni, A., Daniliuc, D., Khurshid, S. and Mariniv, D. (2002) Evaluating the “Small Scope Hypothesis”. POPL Proceedings of ACM Symposium on the Principles of Programming Languages, MA, 1-12.

为你推荐