摘要
幾何命題可能具有多條由已知條件通向結論的推理路徑。如果教師只在一條路徑安排提示,學生仍可循其他路徑完成推理;由此產生一個受成本約束的「提示覆蓋所有路徑」問題。本研究建立一個有限有向無環圖(directed acyclic graph, DAG)中的、由教師預先核實之單前提推理路徑模型:每個合資格的中間推理節點具有非負整數提示成本,任一從起點到終點的路徑必須遇到至少一個提示節點。本文嚴格證明最小成本提示集合與節點拆分網絡的最小割等價,構造能以最小割和可行整數流互相核驗的原始—對偶證書,並在證明圖邊集合只知道上下包絡時,推導最優提示成本的可達上下界及上包絡的安全可行性。在完全人工的九節點示例中,已知圖有六條路徑,其最小提示成本為 6;加入兩條候選推理邊後,上包絡圖有八條路徑,最低安全成本為 11。兩個結果由最大流、128 個子集的獨立枚舉及 220 個隨機小圖的獨立單調性檢查支持。這些運算不測量提示的教學效果,也不證明一般幾何推理必可簡化為單一路徑。本文區分「圖上所有路徑」與「所有真正有效的幾何證明」,其應用前提是教師先行核驗圖的邏輯充分性及路徑完整性。
關鍵詞: 香港中學數學;演繹幾何;多條證明路徑;提示設計;節點最小割;最大流;最優性證書;穩健界
Abstract
A geometric proposition may admit several reasoning paths from assumptions to a conclusion. Placing a hint on one path does not necessarily cover the others. We study a precisely delimited graph abstraction in which an educator has validated a finite directed acyclic graph of single-premise reasoning steps. Eligible intermediate vertices incur nonnegative integer hint costs, and a valid hint set must intersect every source-to-target path. We prove that the minimum-cost hint set is equivalent to a vertex-capacitated minimum cut, describe independently checkable primal–dual certificates consisting of a separating vertex set and a feasible path packing, and establish sharp bounds when the true edge set lies between known lower and upper graphs. An entirely constructed nine-vertex graph contains six paths with optimum cost 6. Adding two possible edges creates an eight-path upper graph with robust cost 11. A maximum-flow implementation and a separate exhaustive enumeration over 128 candidate subsets independently agree; an additional 220 seeded small-graph trials check the monotonicity implication. The examples are mathematical constructions and offer no evidence of classroom effectiveness, student ability, or curriculum endorsement. Inference rules requiring multiple simultaneous premises, unrecorded proof strategies, invalid geometry steps, and unknown hint costs lie outside the claim.
Keywords: Hong Kong secondary mathematics; deductive geometry; proof paths; instructional hints; minimum vertex cut; max flow; optimality certificate; incomplete graphs
1. 引言
香港初中數學課程包含演繹幾何的學習要求;香港教育局亦提供《初中演繹幾何的學與教》教師研習資料,重視前提、結論、邏輯推論與避免循環論證。這一官方背景說明教師需要處理推理結構,但官方文件沒有規定必須以最大流、最小割或任何數學最佳化程序安排提示。本文只把相關題型當成理論應用場景,不擬替代正式課程闡釋或評核要求(香港教育局,2019,2020)。
已有數學教育及自動推理工作探討如何構造幾何題目、尋找學生可理解的證明,以及處理不同的證明鏈(Alvin et al., 2014;Wang & Su, 2015;Font et al., 2020)。若有兩條證明路徑共享某些中間命題,提示同一個共享命題或許可同時接觸數條路徑;相反,不共享節點時,需要多個提示節點。因此「哪個提示成本最低」是明確的組合最佳化問題,可以與「能否自動證明原本的幾何命題」區分處理。
本文的研究問題包括:RQ1,甚麼條件下路徑提示問題可化為加權最小節點截集?RQ2,如何在不信任單一求解器輸出下提供可核驗的最優性證書?RQ3,若教師已記錄一些推理邊,但不能確定是否已列盡,哪些成本及可行性結論仍可保證?RQ4,當提示成本有所變化,最佳決策及核驗界如何變化?
我們把「提示」明確定義為在一個中間節點給予的可辨識文字、圖形或提問。其正整數成本只表示研究者指定的抽象代價,不代表以實驗量得的學生認知負荷、上課分鐘或教師工作量。本模型以能在全部路徑上遇到一個提示為可行性目標,並不保證提示後能完成證明。這種嚴格的目標限制避免把演算法優值偷換成教育成效。
2. 文獻綜述與研究定位
2.1 幾何證明生成與人類可讀性
Alvin、Gulwani、Majumdar 與 Mukhopadhyay(2014)研究由幾何圖形生成高中層次的證明題,顯示計算方法早已用於幾何問題合成。Wang 與 Su(2015)的 iGeoTutor 針對人類可讀的歐氏幾何證明;其原始論文還報告小型學生試用,但並不是香港學生樣本,亦不可轉借其結果證明本方案有效。Font、Cyr、Richard 與 Gagnon(2020)以 Prolog 探討多條幾何證明以及教學情境下的系統困難,最接近本文的「一個命題有多條推導鏈」出發點。
Nirode 與 Boyd(2021)分析美國高中幾何教材給予學生的證明機會與提示支架,但沒有檢驗本模型在香港的教學成效。中文研究方面,李雷、陳矛與彭翕成(2025)使用向量恆等式重組不同幾何題的關係,形成新的證明題。這類工作表明中文領域已研究證明關係的結構表達,但其重點是題目生成,而非已核實推理圖上的最小提示截集。我們只辨認上述已檢索材料中的焦點差異;由於未核讀所有付費全文與學位論文,不能排除存在十分類似的提示最佳化結果。
2.2 最小割方法與學術定位
Ford 與 Fulkerson(1956)已正式建立經典的流與割關係;把節點容量轉為邊容量的節點拆分亦屬成熟網絡最佳化工具。因此,單純將一個圖轉化為最小割,不是原創的圖論定理。本文值得獨立核實的特定組合,是以「教師核准、單前提的證明路徑」為語義假設,明確給出可分別核對的截集與流證書,再加入圖資料不完整時的包絡界與失效條件。這仍屬有限的理論整合與應用推導,尚待更完整的外部新穎性比對。
2.3 文獻比較
表 1:既有文獻的焦點與本文的適用邊界
| 來源 | 已處理的問題 | 本文新增的限定分析 | 不應作出的聲稱 |
|---|---|---|---|
| Alvin et al. (2014) | 幾何證明題的自動生成 | 對已固定的路徑圖計算提示截集 | 首次用電腦處理幾何證明 |
| Wang & Su (2015) | 人類可讀幾何證明系統 | 提示節點的費用與覆蓋可核驗性 | 已證明本文提示能改善學習 |
| Font et al. (2020) | 多證明鏈及 Prolog 推理 | 對有限路徑集進行最小割證書 | 首次提出多證明路徑 |
| 李雷等(2025) | 向量關係與幾何題目合成 | 已審定圖的成本與不完備包絡 | 中文領域未曾研究證明結構 |
| Ford & Fulkerson (1956) | 最大流最小割 | 在特定提示語義下建構可稽核證書 | 發現新的最大流定理 |
| 香港教育局(2019,2020) | 初中數學及演繹幾何學與教背景 | 理論例子可能對課堂討論有用 | 官方認可此演算法 |
3. 理論框架、資料語義與邊界
3.1 具語義限制的推理圖
令有限有向無環圖為 ,起點 代表已知前提已具備的初始狀態,終點 代表欲達成的幾何結論。每條有向邊 只在教師已確認「若命題 已建立,便可依一條單前提的有效規則取得命題 」時成立。可設有一組不合資格節點 (如教師不允許提示的前提或結論);中間合資格集合 中每個節點 有提示代價 。模型假定不重覆計算同一提示,即一個節點只支付一次成本。
關鍵語義告誡。 真實幾何論證常須同時使用兩個或以上前提;例如「兩角及夾邊分別相等」需多個條件共同成立。這是超邊/AND 推理,不能把一個可任意單步通行的普通邊誤當成完整證明。一個一般 AND–OR 證明系統若粗略投影成普通圖,可能產生虛假路徑或遺漏有效推理;下列所有定理只適用於上段定義的單前提語義,或已由邏輯核驗工具正確展開的完整線性證明路徑全集。由於展開可能指數爆炸,本文不宣稱適用於任意幾何題。
令 是 中從 至 的所有有向路徑,對 定義 。若路徑均至少與 有一個相同中間節點,便稱 是一個提示截集。以 的費用最小為目標:
無可行截集時定義 。當 ,空集合自然符合所有條件,故 。若存在一條從 到 的路徑完全不含合資格節點,則沒有任何 能覆蓋它,故 。這包括直接邊 ,但不限於此。
3.2 等價的整數規劃
對 取 ,分別表示不提示/提示,則 (1) 等價於:
式(2)的限制可能有指數個,但不需枚舉全部路徑即可用網絡流求解。其合理性仍依賴路徑與語義完整一致。若費用只含主觀分級、不具可比性,則最小化數值之教育意義無從驗證;目前的抽象代價只用於檢查組合性質。
4. 方法與可重現設計
研究使用四條互補途徑。首先,從式(1)的定義以集合與圖論演繹證明結果,不依賴程式實驗。其次,將每個節點拆成 和 ;只有合資格節點的內部弧容量設為 ,其他弧設定為大常數 。第三,透過增廣路演算法產出最大流、殘量可達集合與最小截集,並獨立檢驗節點截集的可達性及成本。最後,使用不匯入主程式的枚舉核查,對 7 個合資格中間節點的 個子集逐一檢查;另以固定隨機種子建立 220 個小圖,檢查圖包絡的成本單調性。
人工例子由九個標記節點、十三條已知邊及兩條可能增加的邊構成。所有圖的內容、費用、程序、種子與 CSV 均保存於同一資料夾。圖中的 、 都是抽象中間命題代號,不應被看作特定學生的推理步驟;即使以香港幾何課程作背景,亦沒有一個人類受試者。
5. 數學推導、定理與證明
5.1 引理 1:截集與刪節點後的不可達性
引理 1。 對任何 , 與每一條 – 路徑相交,當且僅當在刪除 及其相連邊後的圖 中, 不可從 到達。
證明。 若 仍有一條 – 路徑,該路徑必然避開被刪的全部節點,故 未覆蓋所有路徑。反之,若 未覆蓋所有路徑,便存在一條完全不經 的 – 路徑,刪去 後它仍然存在。兩個方向互為逆否命題,結論成立。證畢。
此引理直接給出可行性證書:提供 及一份從 做圖搜尋的可達集合 ,獨立核查器確認 ,且沒有遺漏從 經合法邊到非 的未刪節點。若只報一個集合而不測試全圖可達性,不能宣稱已覆蓋所有合法路徑。
5.2 定理 1:節點拆分下的最小割等價
定理 1。 對非負整數費用及有限 ,設 ,。把每個 拆為 ,若 ,該內部弧容量為 ;非合資格節點的內部弧容量為 。每條原始邊 對應容量 的 。網絡的源、匯分別取 、,以 表示最小割值。則:
證明。 若存在提示截集 ,在新網絡中刪去 的內部弧,便切斷所有源匯路徑;其總容量為 。因此 。反過來,任何容量小於 的割不能含任何容量 的弧,故只包含合資格節點的內部弧。相應的節點集合 必須割斷所有源匯路徑;由原始圖與拆分圖中路徑一一對應, 為提示截集,且 等於割容量。因而 ,結合先前不等式即得相等。若 卻假設存在有限提示截集,便由其費用不超過 得到矛盾,故無有限可行解。證畢。
零成本邊界。 即使有 ,上述證明仍成立;最小割可為零,也可選含零成本節點的提示。無路徑情形。 若 本來不可達 ,空截集使 。不可提示路徑。 若存在只經不合資格節點的路徑(包括 ),任一源匯割須付至少一條容量 的弧;本研究應輸出「無有限可行截集」,不能把有限數字 誤報為最優成本。
5.3 定理 2:最優性原始—對偶數學證書
在 的所有路徑上設定非負流量 ,限制經每個合資格節點的總流量不大於其成本。此時對每個可行 ,
證明。 由每一條路徑必有至少一個節點在 內,得到 ;交換兩次有限求和得右方 ,再由每節點的容量約束得 。證畢。
定理 2。 若能提供(i)可行提示截集 ,其費用為 ;(ii)一組沿原始圖路徑的非負流量 ,使各合資格節點負荷不大於 、流總量亦為 ,則 必為成本最小的提示截集。對符合定理 1 且有可行截集的網絡,這一對證書可由最大流最小割定理取得。
證明。 由式(4),任何截集 的成本至少是可行路徑流總量 ;而已知 費用恰為 ,因此 。存在性可由拆分網絡的最大流最小割定理證明:其最大流可拆成原始路徑流,節點的流限制正是 ;當容量為整數時,增廣路演算法可選整數增廣量,因而有整數路徑流證書。證畢。
這一證書對驗證十分有用。截集只保證「至多 K」,可行路徑流只保證「至少 K」,當兩者相遇才可斷言最優。若候選流或截集未通過驗證,便不能自稱最優。若真正的證明圖存在未記錄路徑,最優性只對當時指定的圖成立。
5.4 定理 3:不完整推理圖的包絡單調性
保持 固定,考慮三份在同一節點集合上的圖 、 與 ,假設:
定理 3。 若 ,則:
而在上包絡 可行的任意提示截集,對每個滿足式(5)的真實圖 都可行。
證明。 加入邊只會新增或保留既有路徑,不會刪去舊路徑,因此 。能截斷較多路徑的集合必然也能截斷較少路徑;可行解集合從 到 逐步縮小。對同一成本函數取最小,立即得到式(6)。若 能截斷上包絡的全部路徑,則當然截斷其子集 ,故是穩健可行解。證畢。
界的鋒利性。 在只知道式(5)且不附加其他限制時, 和 都是允許的情況;因此一般不能提高下界或降低上界。若 ,便有 (最優值穩健);但若上下界不相等,就不能從已知下包絡的最佳提示集推斷它對未知圖亦可行。
推論 1(穩健額外成本界)。 的最優截集 對任何 可行,且其成本高於該圖未知最優成本的程度至多為:
證明。 由 對 可行及 得第一個不等式。再以 得第二個不等式。證畢。這是在同一指定節點成本表下的數學最優化損失界,並非實際教師工作量或學生表現之估計。
5.5 沒有上包絡時的反例
僅列出已知路徑並不能排除其他新路徑。設下包絡只有 ,合資格節點僅有 ,且 。這時提示 足夠。若真正圖還有直接邊 ,則任何合法提示集合都無法截斷它,最小成本變成 ;即使不允許直接邊,也可加入新中間節點 但規定 不可提示,形成 。所以欠缺可證明的上包絡時,「已列出的一切路徑均覆蓋」無法推出全部真正證明均覆蓋。這不是最大流演算法的錯誤,而是推理圖範圍聲稱失去根據。
5.6 算法複雜度與獨立驗證範圍
拆分網絡有 個節點及 條前向容量弧。使用 Edmonds–Karp 最短增廣路,可於標準多項式時間上界 內求最大流;本稿 Python 程式採用簡單 BFS 增廣法,並從最後殘量圖抽取割。所有成本以整數表示,避免浮點等號比較;實際圖中的成本「1、2、5、9」是人為指定。對小例,第二份程式直接對每個候選集合做可達性搜尋,算術與演算法不依賴主程式。
6. 人工算例、精確結果與圖表
6.1 六條人工路徑與最低提示成本
取已知有向圖,其邊為 ;、、;以及每個 。故恰有六條 – 路徑,分別為 、、、、 與 (每個縮寫路徑均省略共同首尾 )。
表 2:研究者指定的節點成本(人工例子,無實際時間單位)
| 中間節點 | u1 | u2 | u3 | v1 | v2 | v3 | v4 |
|---|---|---|---|---|---|---|---|
| 提示成本 c | 1 | 9 | 1 | 5 | 2 | 2 | 5 |
最優提示候選為 ,成本 。它截斷全部六條路徑;若移去 ,則 可能繞過其餘提示,若移去 ,也有 分支;若移去 或 , 的對應分支不再截斷。這些只是展示此集合不可再刪減的例子,不能單靠不可再刪減證明全局最小,故還需對偶證書。

圖 1:紅色節點是最小提示截集,括號內為人為成本,淺色節點未提示;邊代表假定已核實的單前提推導關係。來源:本文構造及 code/analyse.py;沒有學生測量。
6.2 等值路徑流作為可檢驗的下界
取四個路徑流: 單位走 ; 單位走 ; 單位走 ; 單位走 。各節點的總流量分別不超過表 2 的容量,例如 的負荷為 , 和 各為 ,而 各為 。故有總流量 ,依式(4)所有可行截集費用至少為 ;與 費用 結合,得:
因 只有兩條外分支且 費用大於 ,選 避免昂貴的 ;類似地, 取代 ;最後 的兩條分支可用 各費用 2,共 4,少於 的 9。這是人工圖上的局部直觀;正式全局證明由前段可行截集與流相等支撐。
6.3 加入兩條候選邊所造成的穩健界
假設審定的已知邊集合是 ,而可能尚未記錄的合法邊只有 和 。將兩條均加入取得上包絡 ,此時已知六條路徑增加為八條。上包絡圖中,可用 截斷所有路徑,費用 ;又可在六條允許路徑分別送出 單位流,總量為 11,且各節點負荷不超出表 2 成本(詳見附錄 C)。因此依定理 2,這亦是能獨立檢查的等值最優性證書;128 子集枚舉給出第三種核查。對一切滿足 的未知真實圖:
這表示採用安全上包絡截集最多多付 5 個人為成本單位。下包絡集合 不必對上包絡可行,例如新增 就會繞過 。反過來, 因截住所有第一層中間節點,對任何包絡內候選邊皆可行。

圖 2:固定人工成本時,不完整邊資料容許的最優成本 ;它是確定性集合界,不是信賴區間、概率分布或統計誤差棒。來源:本文解析定理與兩個人工圖的枚舉。
6.4 參數變動下的精確成本結構
把 的費用同步改為 ,保留其餘費用。在此已知圖中, 和 各費用 1,總比透過相應末端分支 、 截集更省;固定這兩節點後,截斷 的路徑可選成本 9 的 ,或合計 的 。由這些分支的全部可能性可直接得到:
可用對 是否選取的分類證明式(10)全域最優。若選 ,左右兩端分支各至少支付 1,選 可達成本 11;若不選 ,必選 ,再支付左右分支各至少 1,故最小成本為 。因此當 時,選 ;當 時,選 ;在 時兩套方案等值。
對上包絡圖,若不選 ,兩條額外邊迫使四個 節點全部被選取,成本為 ;若選 ,左右分支仍各至少支付 1,合計最少為 11。因此對所有非負實數 ,精確公式是 。在 時,選四個 節點最省;當 時,選 最省,於 兩者等值。主程式在整數成本下核算,獨立枚舉另外在有理數格點檢查分數分界點;圖 3 的範圍是 。

圖 3:橫軸 是人為指定的 提示成本;已知圖費用按式(10)分段線性,上包絡圖按 分段線性,分界點為 與 。來源:研究者構造、代數解析及生成程式,非學生心理測量。
6.5 雙程式獨立核查與結果邊界
表 3:可重現結果與未覆蓋範圍
| 核驗方法 | 本次輸出 | 有效範圍 | 不可推論 |
|---|---|---|---|
| 節點拆分 + 整數增廣流 | 已知圖成本 6;上包絡成本 11 | 指定兩個人工 DAG | 教師實際工作量下降 |
| 明示路徑流及截集 | 已知圖 6、上包絡圖 11 的流與割分別等值 | 兩份人工圖的原始—對偶見證 | 任意幾何證明可表為此圖 |
| 不匯入主程式的窮舉 | 兩圖各 128 個集合;唯一最佳截集與主程式吻合 | 7 個可提示節點 | 任意大圖的普遍正確性 |
| 220 個種子固定小圖 | 成本單調性和上包絡截集可行性全數符合 | 指定人工圖生成程序 | 學生樣本統計、置信區間 |
注意,主程式與獨立核查都以標準 Python 整數算術工作,但採不同算法,並非形式證明系統或外部專家。有限計算用於發現程式及示例錯誤,定理的一般性仍來自第 5 節的演繹證明。演算法的任務是找到對已建圖而言正確的截集;未經教師邏輯審定的原始幾何題無法據此得到正式證明。
7. 討論:香港幾何學習中的可能用途
7.1 數學理解:路徑交集比單一路徑更重要
學生常見的證明呈現形式是一串前提、定理及結論,教材若只展示一條標準推導,會隱藏同一命題的其他可能路線。當教師已核實全部課堂允許的路徑後,使用提示截集可以引發一個數學探究:「為何某些共享中間結論比提示各條分支划算?」這可將初中演繹幾何與高中較抽象的圖論、最佳化和對偶思想連結,但仍需按學生年級與課程範圍調整難度;文中網絡流不屬於普通初中學生必須學習的官方規格。
7.2 「成本最低」不等於「教育最好」
本文把每個節點的提示代價當成已知數值。然而在真實課室中,給一個提示是否令學生思維負擔增加、是否掩蓋自行探索的機會,以及是否有利於後續遷移,並沒有由圖上的 決定。若真正要研究教育成效,需要預先註冊的研究問題、倫理批核、適當的對照課堂、學生背景與作答資料、測量信度及不確定性分析。單靠本研究的最佳割,無法建議特定學校採用哪個提示節點。
7.3 證明圖的完整性是瓶頸
已知下包絡的最優成本只能說明所列路徑。如果有另一條尚未記錄的證明,它可以繞過所有已選提示,甚至造成無有限解。實際應用應先由教師明確界定許可定理庫、學生已知條件、允許的推理規則與結論表示,之後核查生成圖與真正推理的對應。即使有上包絡,若包絡含大量不可能的邊,計算出的穩健成本也可能過高;定理 3 則只保證安全,不保證教育可用性。
7.4 可核驗與可解釋的雙重報告
一份可稽核輸出應同時列出提示節點、各節點成本、刪節點後的可達集合,以及足以證明費用不能再降的路徑流。若只有求解器聲稱「最優成本 6」,讀者便無法區分真實最優、軟件錯誤與資料不完備。對 6 的雙證書以及對 11 的窮舉核查,提供教師或研究者自行查證之途徑。這一程序與傳統數學「提出命題、給出可檢查證明」的精神相符,但不是對教學介入成效的驗證。
8. 研究限制
首先,模型的語義很窄,多前提/AND 推理在普通有向圖上的失真是關鍵限制。若以多個前提共同成立作結論,必須使用超圖、推理規則系統或已核實完整的證明展開,不可套用本文的單前提最小割結論。即使推理單步正確,是否所有容許的學生證明已被完整枚舉亦是獨立、一般相當困難的問題。其次,費用是任意人工數值,不具任何心理測量單位。再次,最多 7 個提示節點的窮舉只是示範驗證,220 次種子固定小圖不是大規模形式化驗證,也不是統計樣本。最後,本文的關鍵數學等價直接來自經典最小割;本研究的理論整合可能與既有教學輔助研究重疊,仍須系統性文獻比較及外部審查。沒有倫理批核或真實學生資料,不能估算香港學習效果、對公平性的影響或 HKDSE 表現差異。
9. 結論
在經核准的有限、單前提推理圖內,要求每條證明路徑至少經過一個提示節點,可精確寫為加權節點截集。節點拆分與最大流最小割為其提供多項式時間求解及原始—對偶等值證書;若未知圖介乎下包絡與上包絡之間,最優成本會被兩端包住,上包絡的截集保證對所有容許未知圖可行。人工六路徑例子的成本 6、加入候選邊後的成本 11,以及相應的窮舉核查,都只支持指定數學模型。後續值得研究的方向是 AND–OR 證明超圖的提示選擇、成本不確定性的決策理論、以及在完成倫理審批後對真實教學策略所作的獨立實證研究。
參考文獻
Alvin, C., Gulwani, S., Majumdar, R., & Mukhopadhyay, S. (2014). Synthesis of geometry proof problems. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1). https://doi.org/10.1609/aaai.v28i1.8745
Font, L., Cyr, S., Richard, P. R., & Gagnon, M. (2020). Automating the generation of high school geometry proofs using Prolog in an educational context. Electronic Proceedings in Theoretical Computer Science, 313, 1–16. https://doi.org/10.4204/EPTCS.313.1
Ford, L. R., Jr., & Fulkerson, D. R. (1956). Maximal flow through a network. Canadian Journal of Mathematics, 8, 399–404. https://doi.org/10.4153/CJM-1956-045-5
Nirode, W., & Boyd, B. (2021). High school geometry textbooks’ proving opportunities of Common Core theorems. School Science and Mathematics, 121(6), 345–356. https://doi.org/10.1111/ssm.12487
Wang, K., & Su, Z. (2015). Automated geometry theorem proving for human-readable proofs. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (pp. 1193–1199). https://www.ijcai.org/Proceedings/15/Papers/172.pdf
李雷、陳矛、彭翕成(2025)。基於向量恆等式的幾何證明題自動生成方法。《計算機工程》,51(7),78–89。https://doi.org/10.19678/j.issn.1000-3428.0068959
香港教育局(2019)。《中學數學課程修訂簡介及初中演繹幾何的學與教》(教師專業發展研討會簡報)。https://www.edb.gov.hk/attachment/tc/curriculum-development/kla/ma/res/ss/SS%20handout%20RevSec%2001%20Ded%20Geo.pdf
香港教育局(2020)。《初中數學課程闡釋》。https://www.edb.gov.hk/attachment/tc/curriculum-development/kla/ma/curr/EN_KS3_tc.pdf