《有限制條件的幾何定理機器證明》是依託華中師範大學，由陳矛擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：有限制條件的幾何定理機器證明
- 項目類別：青年科學基金項目
- 項目負責人：陳矛
- 依託單位：華中師範大學
項目摘要,結題摘要,
項目摘要
中學幾何教學對具有幾何定理自動推理功能的智慧型教育軟體有強烈需求，但現有幾何定理機器證明的研究成果還不能滿足中學幾何教學的實際需求。為了充分挖掘幾何定理機器證明的教學價值，滿足中學幾何教學的實際需求，本項目開展有限制條件的幾何定理機器證明研究，在提高算法推理能力使之能滿足教學需求的同時，對算法的推理規則、證明的長度和證明的表達形式等進行限制。主要研究內容包括(1)將向量法、輔助線法和反證法等中學課本上的證題方法設計為算法；(2)設計推理規則庫和謂詞庫；(3)將前推法和後推法結合起來形成一個雙向搜尋算法；(4)設計算例庫，對有限制條件的幾何定理機器證明算法進行測試。本項目可進一步深入研究幾何定理機器證明，也將對數學機械化在幾何教學中的套用起到一定推動作用，為設計開發智慧型教育軟體奠定理論和技術基礎。
結題摘要
中學幾何教學對具有幾何定理自動推理功能的智慧型教育軟體有強烈需求，但現有“幾何定理機器證明”的研究成果還不能滿足中學幾何教學的需求。本項目系統深入地開展有限制條件的“幾何定理機器證明”研究，旨在充分挖掘“幾何定理機器證明”的教學價值，滿足中學幾何教學的需求。本項目在分析中學幾何定理以及推理法、添加輔助線法和向量法等幾何證明常用方法的基礎上，將這些幾何定理和證題規律總結為一系列謂詞和推理規則，並將前推法和後推法結合起來，設計了一個高效的雙向搜尋算法。在算法設計中，我們對算法的推理規則、證明的長度和證明的表達形式等進行限制，使之不超出中學幾何教學大綱的範疇，以充分滿足實際教學的需求。為驗證本項目給出的算法和方法，我們研發了一款幾何定理自動推理原型系統，並基於中學幾何課本上的練習題、習題集和數學競賽題設計了一套測試算例集。測試結果表明，本項目給出的自動推理算法能對算例集中82%的題目給予成功證明。除了一些較難的競賽題，絕大多數題目的推理長度不超過13步，推理時間在3秒以內，可滿足中學幾何教學的實際需求。基於幾何定理自動推理過程中形成的推理鏈，我們還研究了幾何證明題的自動出題及解答驗證機制，實現了包括填空、判斷、選擇、計算和證明等多種題型在內的自動出題和解答驗證功能。本項目的研究成果豐富了幾何定理機器證明研究的方法和手段，對數學機械化在幾何教學中的套用起到一定推動作用，為設計開發數學學科相關的智慧型教育軟體奠定了理論和技術基礎。
