基于Alloy的7₃构形存在性定理的机器验证

Machine Verification of the Existence Theorem of Configuration 7₃ Based on Alloy

73构形的存在性是有限几何中的一个基本问题。本文给出了一种用Alloy分析器自动验证73构形的存在性的方法。该方法使用 Alloy语言对Fano提出的公理系统和需要验证的定理进行形式化,然后利用Alloy分析器分析定理是否满足属性要求。实验结果表明本文提出的机器验证方法是可行的。

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.