基于Alloy的有限几何定理的机器验证

发布时间：2020-07-13 03:11

【摘要】：定理机器验证是自动推理领域内的一个重要研究课题,其研究方法和研究成果具有十分显著的理论意义与应用价值。目前研究者们已成功验证了数学中一些较为复杂的定理和猜想问题,例如四色定理、Kepler猜想以及李群_8E结构等。这些工作不仅推动了数学领域中定理机器验证的研究,也对其他领域定理的研究提供了有利的帮助。有限几何定理由于点线关联结构复杂多样化的特点引起了研究者们的关注。目前,研究者们已编写出一些验证有限几何定理的计算机程序,但这些程序运行时间较长,可读性较差,同时程序的语法相对繁琐复杂,不易于理解,导致研究者们关于这些程序的研究并无太大进展,致使有限几何定理的机器验证也无较大的发展。本文提出利用Alloy验证有限几何定理的新方法。该方法的的优点是:语言精练简洁,易于理解,表达能力较强,程序相对简单,同时验证效率较高,验证结果可读性较好。本文对有限几何中的n阶射影平面存在性定理和n阶仿射平面存在性定理进行了机器验证。基本步骤为首先用Alloy建模语言对这两类定理进行建模,然后借助于Alloy分析器对模型进行自动化分析。验证结果表明,该方法不仅效率高,而且可读性较强,同时还能够给出具体平面存在的可视化实例。本文提出的方法为我们研究有限几何定理中结构较为复杂的开问题提供了一个新的验证思路。
【学位授予单位】：辽宁师范大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：O18
【图文】：

射影平面,定理

图 3.1 退化射影平面Fig.3.1 Degradation projective plane2），如果我们将点作为直线，将直线作为有限射影平面中的重要定理。有限射影平面的一个定理， A *为将 A中 A *也是关于有限射影平面的一个定理。L,I 为有限射影平面，则在L中存在这样 4平面中的任意一条直线都至少包含三点。平面上有一条直线恰好包含 n 1个点，有限射影平面，若其中有一条直线恰好包.3 及定义 3.5，我们可以得到如下的定理。n阶射影平面，则 n 2，且

射影平面,检测结果,反例

assert theorem2order{# Point = 7# Line = 7}check theorem2order for 10 Point ,10 Line 命令用来检测断言是否是成立，因为 Alloy 分析器是在有限的范围内查用 check 命令检测时要指定签名的个数，如：check theorem2order forine，表示在 Point 10，Line 10 的范围内搜索满足断言的实例。如果不会产生反例，如果断言不成立，系统会产生一个违反断言的实例，即，我们可由提供的反例快速找到具体错误的来源。的验证中，我们使用系统默认的 SAT4J 求解器，经过 218ms 的求解后unterexampie found”，即无反例产生，可以基本确定该定理是成立的

实例图,射影平面,实例,可视化

图 3.3 2 阶射影平面存在的可视化实例Fig.3.3 A visual example of projective plane of order 2由图 3.3 知，它含有 7 个点和 7 条直线，每条直线上有 3 个点，每个点都与 3 条直线关联。分析后的图形如图所示：图 3.4 二阶射影平面Fig.3.4 Projective plane of order 2图 3.4 为 2 阶射影平面存在的实例，直线与点关联的结构为 0L P 4, P 5, P6， 1L P 2, P 3, P6， 2L P1 , P 3, P5, 3L P1 , P 2, P4 4L P 0, P 3, P4， 5L P1 , P 0, P6

【参考文献】