【摘要】：定理機器驗證是自動推理領域內(nèi)的一個重要研究課題,其研究方法和研究成果具有十分顯著的理論意義與應用價值。目前研究者們已成功驗證了數(shù)學中一些較為復雜的定理和猜想問題,例如四色定理、Kepler猜想以及李群_8E結構等。這些工作不僅推動了數(shù)學領域中定理機器驗證的研究,也對其他領域定理的研究提供了有利的幫助。有限幾何定理由于點線關聯(lián)結構復雜多樣化的特點引起了研究者們的關注。目前,研究者們已編寫出一些驗證有限幾何定理的計算機程序,但這些程序運行時間較長,可讀性較差,同時程序的語法相對繁瑣復雜,不易于理解,導致研究者們關于這些程序的研究并無太大進展,致使有限幾何定理的機器驗證也無較大的發(fā)展。本文提出利用Alloy驗證有限幾何定理的新方法。該方法的的優(yōu)點是:語言精練簡潔,易于理解,表達能力較強,程序相對簡單,同時驗證效率較高,驗證結果可讀性較好。本文對有限幾何中的n階射影平面存在性定理和n階仿射平面存在性定理進行了機器驗證�；静襟E為首先用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 分析器是在有限的范圍內(nèi)查用 check 命令檢測時要指定簽名的個數(shù)，如：check theorem2order forine，表示在 Point 10，Line 10 的范圍內(nèi)搜索滿足斷言的實例。如果不會產(chǎn)生反例，如果斷言不成立，系統(tǒng)會產(chǎn)生一個違反斷言的實例，即，我們可由提供的反例快速找到具體錯誤的來源。的驗證中，我們使用系統(tǒng)默認的 SAT4J 求解器，經(jīng)過 218ms 的求解后unterexampie found”，即無反例產(chǎn)生，可以基本確定該定理是成立的

圖 3.3 2 階射影平面存在的可視化實例Fig.3.3 A visual example of projective plane of order 2由圖 3.3 知，它含有 7 個點和 7 條直線，每條直線上有 3 個點，每個點都與 3 條直線關聯(lián)。分析后的圖形如圖所示：圖 3.4 二階射影平面Fig.3.4 Projective plane of order 2圖 3.4 為 2 階射影平面存在的實例，直線與點關聯(lián)的結構為 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

【參考文獻】

相關期刊論文 前4條

1 楊家海;姜寧;安常青;李福亮;;基于形式化描述的交換機網(wǎng)絡自動配置策略的設計與實現(xiàn)[J];清華大學學報(自然科學版);2012年08期

2 鄧米克;THE PARALLEL NUMERICAL METHOD OF PROVING THE CONSTRUCTIVE GEOMETRIC THEOREM[J];Chinese Science Bulletin;1989年13期

3 洪加威;能用例證法來證明幾何定理嗎?[J];中國科學(A輯 數(shù)學 物理學 天文學 技術科學);1986年03期

4 吳文俊;初等幾何判定問題與機械化證明[J];中國科學;1977年06期

本文編號：2752872