Minimum-Cost Hint Interception in Multi-Premise Proofs for Hong Kong Deductive Geometry: Horn Semantics, Complexity Boundaries and Verifiable Certificates

摘要

香港初中演繹幾何的推理往往同時需要多個前提，亦可能透過不同定理得出同一結論。將多前提規則拆成普通圖邊可能虛構不存在的證明路徑，令提示選點最優解失去語義基礎。本研究建立有限 Horn 式 AND–OR 證明模型：由前向推理的最小不動點定義可推導性，並以刪除合資格中間命題的數學代理操作界定「擊中全部證明樹」，每個命題具有指定的非負抽象成本。我們嚴格證明閉包不可達與擊中所有有限良基證明樹等價，並轉化為加權證明支撐集擊中集問題。以 Vertex Cover 作保持最優值的歸約，即使每條規則最多兩項前提且推理系統無環，最小提示截樹的決策版本仍為 NP-complete；而兩層二分交互的限定子類可由最大流／最小割給出整數最優性證書。一般系統可透過分數證明樹打包取得下界，但完整圖 K_n 的整數／線性鬆弛差距趨近 2。本文另證明費用敏感度界及未知規則集的單調上下包絡，提出含兩條合法推理路徑的等腰三角形示例。260 組二分人工圖、240 組一般小型 Horn 人工案例的獨立算法比對支持有限程式一致性。結果屬數學模型分析，不構成教學有效性或新的普遍圖論定理之證據。

關鍵詞： 香港中學數學；演繹幾何；Horn 規則；AND–OR 證明；提示截樹；加權擊中集；頂點覆蓋；最優性證書

Abstract

Multi-premise deduction is central to geometry proofs, which may also admit alternative arguments. Replacing an AND rule by independent graph edges can introduce spurious proof paths. We model a finite Horn-style AND–OR proof system in which selected intermediate propositions are intercepted at abstract nonnegative costs. We prove that removing a candidate set makes the target underivable exactly when the set intersects every finite well-founded proof tree, and reformulate the task as weighted hitting set over proof supports. An optimum-preserving reduction from Vertex Cover shows NP-completeness even with at most two premises per rule and an acyclic derivation structure. A precisely defined bipartite two-layer subclass admits integral min-cut/max-flow certificates. Fractional proof-support packing gives valid lower bounds for general instances; complete graphs exhibit integrality gaps approaching two. We further derive cost-sensitivity and rule-uncertainty bounds and present a constructed isosceles-triangle example with two valid arguments. Two independently designed numerical audits check 260 synthetic bipartite graphs and 240 general Horn systems. This theoretical adaptation of existing combinatorial methods offers no evidence of classroom effectiveness, measured hint difficulty, or originality of the underlying graph theorems.

Keywords: Hong Kong mathematics education; deductive geometry; AND–OR proofs; Horn logic; weighted hitting set; maximum flow; verifiable optimization

1. 引言

香港教育局修訂初中數學課程將演繹推理融入全等三角形、相似三角形、四邊形及三角形中心等內容；教育局亦在 2019 年教師研習材料介紹初中演繹幾何。這說明證明推理結構與香港中學課程具有明確關聯，卻不意味教育局認可本研究的最佳化方法（香港教育局，2019，2020）。例如要以 SAS 證明兩三角形全等，必須同時建立兩組邊相等與夾角相等；一組條件單獨成立不能導出全等。若把每個前提各畫成一條可自由通行的普通圖邊，可能出現假的通路。

系列前作 HKME-005 在教師核實的單前提 DAG 上，以節點拆分與最大流處理所有路徑的最小提示截集。但一般幾何證明有「全部前提同時成立」的 AND 邏輯，以及「任一證明方法均可使用」的 OR 邏輯，因此本文正面處理多前提規則、可推導性的嚴格語義，以及普通最大流方法失效的原因。

研究問題為：RQ1，哪些情況下有限證明樹與前向閉包嚴格等價？RQ2，為何僅容許二前提即可能出現 NP-complete，而某些有結構的子類仍可精確求解？RQ3，如何區分上界可行性證書、對偶下界證書與真正最優證書？RQ4，成本及尚未確認的推理規則改動後，可保持哪些數學保證？

本文「刪除提示節點」是計算代理語義：把所選命題視為需要提示而不再容許作為「無需提示的完整推導」中的節點。真實提供提示可能協助學生完成證明；本文並不研究這個因果效果。人工指定的成本亦不是認知負荷、課堂分鐘或任何量表。

2. 文獻綜述與新穎性定位

Gallo、Longo、Pallottino 與 Nguyen（1993）系統處理有向超圖、路徑、割及 AND–OR 圖的相關應用；本文使用已知的超圖表示，不聲稱發明這套表示法。Reiter（1987）提出系統診斷的邏輯框架，Peñaloza（2020）整理 axiom pinpointing 中關於公理如何支持某個結論的研究，兩者顯示「找出支持集並擊中所有支持」不是新問題。Bläsius 等（2022）對超圖極小擊中集的枚舉有正式理論及演算法結果，也限制本研究的原創性宣稱。

Karp（1972）是 Vertex Cover NP-complete 的經典來源，而加權二分頂點覆蓋的流割轉換亦屬成熟演算法。2026 年 Yao 等提出的 CoCo-Prover 預印本使用 AND–OR 證明超圖描述形式驗證的自動化資源成本，與本文課堂提示語義不同，但說明「證明超圖上帶成本的選擇」已有近年直接研究，不能聲稱全新。Hein 與 Prediger（2024）的設計研究指出，證明邏輯結構的圖像支架需要與語言支援配合；該研究有自己的教學資料，而本文沒有任何學生觀察，不能借用其結果作有效性聲明。

表 1：相關研究與本文的定位限制

來源	既有貢獻	本文借用及未處理之處
Gallo et al. (1993)	有向超圖、AND–OR 及割	使用既有表示；未創立超圖理論
Reiter (1987); Peñaloza (2020)	診斷及邏輯支撐／公理定位	擊中全部證明支撐早有先例
Karp (1972); Bläsius et al. (2022)	Vertex Cover 複雜度；擊中集枚舉	本文用既有定理研究限定教育語義
Hein & Prediger (2024)	證明邏輯之圖像與語言支架研究	未驗證本文提示對學生之效果
Yao et al. (2026)	形式驗證的 AND–OR 與代理成本	不同成本意義；本稿仍須查重
香港教育局（2019，2020）	香港初中演繹幾何課程與教師資源	僅供課程相關性背景

本輪閱讀包含原始論文摘要、部分開放全文、機構書目及官方資源，並非完整系統性文獻回顧。特別是 Horn 公理刪除、hypergraph interdiction 與 ontology diagnosis 已有直接先例，故本文的新穎性只宜描述為在香港幾何提示語義下有明確限制的數學整合與可重現證書；沒有證據支持全球首次發明這個最佳化問題。

3. 有限 Horn 式證明樹的語義

3.1 規則、候選節點與固定點

設有限命題集合為 $V$ ，初始事實為 $I\subseteq V$ ，目標 $t\in V\setminus I$ 。規則 $(A,b)$ 由前提集合 $A\subseteq V$ 及單一結論 $b\in V$ 組成；全部 $A$ 同時成立才可推出 $b$ ，容許 $A=\varnothing$ 表示公理，也容許不同規則導出同一結論與循環規則。合資格提示節點 $H\subseteq V\setminus\{t\}$ 具有非負成本 $c:H\to\mathbb R_{\ge0}$ 。所有規則應由幾何教師或可信邏輯系統事先核實其有效性；本研究未完成此項外部核實。

對 $X\subseteq H$ ，從 $I\setminus X$ 開始，以如下前向規則逐步擴張：

C_0(X)=I\setminus X,\quad C_{k+1}(X)=C_k(X)\cup\{b\in V\setminus X:(A,b)\in R,\ A\subseteq C_k(X)\}.\tag{1}

因集合有限且序列單調，至多 $|V|$ 次嚴格增加便達最小固定點 $C(X)$ 。定義最小提示截樹成本：

\tau(R,c)=\min_{X\subseteq H}\{c(X):t\notin C(X)\},\quad c(X)=\sum_{v\in X}c_v,\quad\min\varnothing=+\infty.\tag{2}

「無法截樹」與「最小成本為 0」必須區分：前者意謂對全部候選集合目標仍可推導，後者可能是本來不可推導，也可能選到零成本節點。成本不必為整數才可定義最優解；只有流的整數性聲明須額外限制容量。

3.2 證明樹與閉包的精確等價

一棵以命題 $b$ 為根的有限證明樹，其葉子必為 $I$ 中事實或空前提規則之結論；每個內部節點 $v$ 的兒子集合必恰為某條合法規則 $(A,v)$ 的完整前提集合。允許同一命題在不同樹枝重覆出現，但不允許以無根據無窮循環冒充一個有限良基證明。

定理 1（閉包—證明樹等價）。 任意 $X\subseteq H$ ， $t\in C(X)$ 當且僅當存在一棵完全避開 $X$ 的有限合法 $t$ -證明樹。

證明。 假設 $t$ 在閉包第 $k$ 層首次出現。對層數歸納：第 0 層為初始事實，可以作單節點樹；較高層必由規則 $(A,t)$ 導出，且全部前提在更低層已出現。對每項前提接上歸納所得子樹，便形成一棵有限避開 $X$ 的證明樹； $A=\varnothing$ 自動對應公理葉子。反向對樹高度歸納，所有葉子可導出；若某內部節點的全部兒子已在閉包，其完整規則保證父節點也加入閉包；故根 $t$ 可導出。有限良基的層數歸納排除無根據的自我循環。證畢。

令 $S(T)=H\cap\{\text{樹 }T\text{ 使用過的命題}\}$ ， $\mathcal S=\{S(T):T\text{ 為有限 }t\text{-證明樹}\}$ ；即使樹數目很多，支撐集仍是有限集合 $2^H$ 的子族。定理 1 等價於下列擊中集模型：

\tau(R,c)=\min_{X\subseteq H}\{c(X):X\cap S\ne\varnothing\ \ \forall S\in\mathcal S\}.\tag{3}

命題 1（可行性先檢）。 存在有限截樹集合，當且僅當 $t\notin C(H)$ 。理由是 $C(H)\subseteq C(X)$ 對任何 $X\subseteq H$ 成立：刪除更多命題只能減少可推導的結論；若移除全部候選命題後仍可推導，任何部分選取皆不可能成功。

反例 1（把 AND 當 OR）。 設 $I=\{s\}$ ，規則為 $\{s\}\to a$ 與 $\{a,b\}\to t$ ，而 $b$ 不可推導。真正 Horn 模型的 $t$ 無法得到，空集合費用 0 已足夠；把第二規則拆成 $a\to t$ 、 $b\to t$ 會虛構一條 $s\to a\to t$ 路徑，錯誤要求購買 $a$ 的提示。錯誤出於語義轉換，不能歸咎於最短路或最大流算法。

4. 研究方法與證據種類

理論部分直接依集合歸納、複雜度歸約與網絡流割證明結果；所有計算僅是人工有限個案的獨立驗證。主程式 code/pilot.py 以前向 Horn 閉包和提示集合窮舉計算，對特殊二分構造另設純 Python 殘量網絡最大流。code/independent_audit.py 不匯入主程式，而依邊的端點是否被選來逐個枚舉合法 Vertex Cover。額外的 code/expanded_audit.py 則枚舉有限證明樹的合資格節點支撐集，把它們作為擊中集約束，與另一組閉包枚舉所得最優解交叉核查。後者的驗證方式不同於逐步前向推理：它由推理樹子樹之聯集固定點生成所有支撐，再對每個介入集合測試其是否擊中各個支撐。

主要測試使用兩個固定隨機種子。二分實驗以 2026101506 生成 260 張左右各三個節點之人工二分圖，每條可能邊出現機率 0.47，節點成本在 0 至 8 之間。一般 Horn 實驗以 20261015061 生成 240 個六命題小系統，四個候選提示命題、每條規則 0–2 個前提，容許空前提規則、循環、零成本與重覆規則。後者每個例子檢查全部 16 個候選介入集合。這些隨機資料只用於軟件實現核查，既不是香港學生樣本，也不是可推斷任何教育參數的蒙地卡羅估計。

論文同時給出三個層級的可核驗聲明：一是刪除候選集合後目標不可達的可行上界；二是任何分數證明樹打包提供的數值下界；三是在適用範圍內上、下界相等的最優性證書。當上、下界不相等時，只能承認仍存在最優性缺口。

5. 數學推導與定理

5.1 至多二前提、無環系統的 NP-completeness

定理 2（保持成本的 Vertex Cover 歸約）。 在命題、規則與預算以有限字串編碼、費用為二進位表示的非負整數（或有理數）的計算問題中，給定預算 $B$ ，判定是否存在滿足 $c(X)\le B$ 的可行截樹集合，為 NP-complete。即使 (i) 每條規則最多兩項前提，(ii) 規則依賴無環，(iii) 只有一個初始事實，(iv) 所有合資格節點成本皆為 1，結論仍成立。任意實數費用的抽象數學模型不附帶有限位元輸入編碼，故不以此宣稱其一般計算複雜度屬 NP。

證明。 從任意無向圖 $F=(U,E)$ 的 Vertex Cover 實例構造 $V=U\cup\{s,t\}$ 、 $I=\{s\}$ 、 $H=U$ 。每個頂點 $u$ 對應規則 $\{s\}\to u$ ，每條無向邊 $\{u,v\}\in E$ 對應雙前提規則 $\{u,v\}\to t$ 。全部頂點由 $s$ 可得到；刪除 $X$ 後，仍可導出的中間命題恰為 $U\setminus X$ ，故 $t$ 可導出當且僅當存在一條邊的兩個端點都未被選。因此 $t\notin C(X)$ 當且僅當 $X$ 為圖 $F$ 的 Vertex Cover，而所需費用恰等於覆蓋的節點數。構造大小為 $O(|U|+|E|)$ ，依賴從 $s$ 經 $U$ 指向 $t$ ，沒有環。Vertex Cover 為經典 NP-complete 問題（Karp, 1972），故本問題 NP-hard。另一方面，給定 $X$ 以多項式次前向閉包迭代核查 $t\notin C(X)$ 並計算 $c(X)$ ，可在多項式時間內驗證證書，故屬 NP。證畢。

\tau(R_F,\mathbf 1)=\min\{|X|:X\subseteq U,\ \{u,v\}\in E\Longrightarrow (u\in X\ \text{或}\ v\in X)\}.\tag{4}

此歸約將經典頂點覆蓋直接嵌入本研究之提示語義，是清楚展示 HKME-005 普通最小割推廣限制的方式，並非發現了此前未知的 NP-hard 問題。NP-complete 是最壞情況複雜度，不代表小型實際幾何證明必難以求解。

5.2 二分交互的特別結構與等值流證書

定理 3（二層二分子類）。 在定理 2 的同一構造下，若 $F=(L\sqcup D,E)$ 為二分圖，成本 $c_v$ 為非負整數，則可建源 $q$ 、匯 $z$ 的網絡： $q\to\ell$ 容量 $c_\ell$ （ $\ell\in L$ ）， $\ell\to d$ 容量 $M=1+\sum_{v\in U}c_v$ （ $\{\ell,d\}\in E$ ）， $d\to z$ 容量 $c_d$ （ $d\in D$ ）。最佳截樹成本、網絡最小割容量與最大流值相等，並可取整數流。

\tau(R_F,c)=\min_{X\text{ 為 }E\text{ 的頂點覆蓋}} c(X)=\min_{\text{割 }(S,\bar S)}\mathrm{cap}(S,\bar S)=\max_f |f|.\tag{5}

證明。 直接選取 $L$ 的全體或 $D$ 的全體都是合法 Vertex Cover，費用不超過 $\sum c_v<M$ ，故最小割必不跨越任何容量 $M$ 的中間弧。對這類割，令 $S$ 為源側頂點集合，選 $X=(L\setminus S)\cup(D\cap S)$ 。若存在一條原邊 $\{\ell,d\}$ 的兩端均未被選，則 $\ell\in S$ 、 $d\notin S$ ，其容量 $M$ 的弧跨割，矛盾。因此 $X$ 是覆蓋，割容量正好等於 $c(X)$ 。反向任取一個覆蓋 $X$ ，令 $S=\{q\}\cup(L\setminus X)\cup(D\cap X)$ ，因每條原邊至少一端被選，中間容量 $M$ 的弧均不跨割，割費用正好 $c(X)$ 。兩類最優值因此相等；再由已知最大流最小割定理及整數容量的整數流性，得到式（5）。證畢。

這個二分條件只針對由圖 $F$ 編碼的特殊兩層二前提構造，不是對任何可以畫成上下兩排的證明超圖均成立。加入第三層重用命題、不同結論的多條 AND 超規則或跨層推理後，不能假設仍可使用同一流割網絡。

圖 1：多前提 AND 與多規則 OR 的邏輯示意；全部命題均為研究者構造。

表 2：人工二分交互構造與最優解

類別	人工輸入	成本／結果
左側候選	$a,b$	$c_a=2,\ c_b=3$
右側候選	$c,d$	$c_c=2,\ c_d=1$
雙前提	$\{a,c\}\to t,\ \{a,d\}\to t,\ \{b,d\}\to t$	所有規則皆有兩項前提
單前提	$s\to a,b,c,d$	$I=\{s\}$
合法最佳截樹集	$\{a,d\}$ 或 $\{c,d\}$	最佳值 3
數值證書	二分最小割 3；最大流 3	上、下界同值

不論以哪個最佳集合，三棵簡單證明樹均被擊中；算法可能回傳其中一個最佳集合。不能把多解誤報成唯一最優。

5.3 證明支撐集的整數規劃、對偶與界

設 $\mathcal S$ 為定理 1 的所有有限證明樹的不同支撐集合。令 $x_v=1$ 表示選提示，否則為 0，則式（3）等價於整數規劃：

\min_x\sum_{v\in H}c_vx_v\quad\mathrm{s.t.}\quad\sum_{v\in S}x_v\ge1\ (S\in\mathcal S),\quad x_v\in\{0,1\}.\tag{6}

把整數性放鬆為 $x_v\ge0$ 得到 LP，對每個支撐 $S$ 引入非負打包變量 $y_S$ ，其對偶為

\max_{y\ge0}\sum_{S\in\mathcal S}y_S\quad\mathrm{s.t.}\quad\sum_{S\ni v}y_S\le c_v\ (v\in H).\tag{7}

命題 2（分數打包下界）。 任何可行截樹集 $X$ 、任何滿足式（7）的 $y$ ，都有

\sum_{S\in\mathcal S}y_S\le\mathrm{LP}\le\tau(R,c)\le c(X).\tag{8}

證明。 每個支撐至少遇到 $X$ 一次，故 $\sum_Sy_S\le\sum_S y_S\sum_{v\in X\cap S}1=\sum_{v\in X}\sum_{S\ni v}y_S\le\sum_{v\in X}c_v$ 。LP 最優值不會超過施加整數性後的最佳值，任何整數可行集合的費用又是最佳值的上界。特別地，若上下界相等，則已有可檢查的最佳值證書；若不同，差額便是未解決的最優性缺口。證畢。

若存在不含任何合資格節點的證明樹， $\mathcal S$ 包含空集合，式（6）的條件 $0\ge1$ 不可行，與命題 1 一致。即使支撐集總數有限，它也可能隨命題數目指數增長，實際認證一份對偶解時須核查所有相關容量制約；不能只列幾棵樣本樹便宣稱完成所有約束核查。

定理 4（完整圖的整數差距）。 若第 5.1 節構造的原圖是 $K_n$ （ $n\ge3$ ），所有成本為 1，則整數最優為 $n-1$ ，LP 最優為 $n/2$ ，其比值趨近 2。

證明。 若留下至少兩個未被選的頂點，它們之間必有邊不被擊中，所以必須選最少 $n-1$ 個頂點；選取恰 $n-1$ 個亦可行。對 LP，令所有 $x_v=1/2$ ，每條邊的限制 $x_u+x_v\ge1$ 都取等號，總費用 $n/2$ 。反向把 $\binom n2$ 條邊的 LP 限制相加，每個頂點變量恰出現 $n-1$ 次，得 $(n-1)\sum_v x_v\ge\binom n2$ ，即 $\sum_vx_v\ge n/2$ 。兩向相同，證明 LP 最優值為 $n/2$ 。證畢。

\frac{\tau(K_n)}{\mathrm{LP}(K_n)}=\frac{n-1}{n/2}=2-\frac2n.\tag{9}

三角形 $K_3$ 的整數成本是 2，分數放鬆成本為 $3/2$ ，整數差距為 $4/3$ 。此下界 1.5 不能被錯稱為一個可實際選出的整數提示集合。圖 2 根據式（9）展示 $n=3$ 至 9 的解析值，而非教學觀察值。

圖 2：完全圖 K_n 的整數與 LP 最佳值比例，全部數字來自解析式。

5.4 成本變動的界與一個封閉式例子

固定規則與合資格節點、假設可行， $\tau(c)$ 是有限個非負係數線性費用函數的逐點最小值：

\tau(c)=\min_{X:t\notin C(X)}\sum_{v\in X}c_v.\tag{10}

命題 3（費用敏感度）。 最佳費用在非負成本正交區域內對各座標非遞減、連續、分段線性且為凹函數；任意兩組費用 $c,d$ 有 $|\tau(c)-\tau(d)|\le\sum_{v\in H}|c_v-d_v|$ 。

證明。 對每個固定合法截樹集，費用是係數為 0 或 1 的線性函數，有限線性函數的最小值為凹、連續的分段線性函數；各座標增大不會使任一合法集合費用下降。若 $X_d$ 是 $d$ 下的最佳集合，則 $\tau(c)\le c(X_d)\le d(X_d)+\sum_v|c_v-d_v|=\tau(d)+\|c-d\|_1$ 。交換 $c,d$ 取得反向界，完成證明。

表 2 中只把 $a$ 的成本改成 $x\ge0$ ，其它 $b,c,d$ 費用分別固定為 3、2、1。要擊中 $\{b,d\}$ 必須選 $b$ 或 $d$ ；比較 $\{a,d\}$ 與 $\{c,d\}$ 及含 $b$ 的其它覆蓋，得到

\tau(x)=\min\{x+1,3\},\quad x\ge0.\tag{11}

當 $x<2$ 以 $\{a,d\}$ 為最佳； $x>2$ 時 $\{c,d\}$ 最佳； $x=2$ 時兩者同價 3。這是人工費用的解析轉折，並無任何學生心理測量單位。圖 3 顯示整數格點 0 至 20 的兩種算法核驗與解析曲線。

圖 3：二分人工例子中的成本敏感度，來源：式（11）及程式核驗。

5.5 未完整列舉的規則集之安全包絡

定理 5（規則集合之單調性）。 固定 $V,I,t,H,c$ ，若 $R_L\subseteq R_*\subseteq R_U$ ，則對任意 $X\subseteq H$ ，其閉包及最佳值滿足：

C_{R_L}(X)\subseteq C_{R_*}(X)\subseteq C_{R_U}(X),\quad\tau(R_L,c)\le\tau(R_*,c)\le\tau(R_U,c).\tag{12}

證明。 對式（1）的迭代層數歸納：規則增加只能加入新的可推導命題，不會令已有命題消失。故最小固定點保持集合包含。截斷較多規則所需的提示集合，亦必能截斷較少規則的系統，因此可行集合族反向包含，最優費用依規則數目非遞減。令不可行時最佳值為 $+\infty$ ，擴展實數次序仍使不等式成立。證畢。

若上包絡有可行截樹集 $X_U$ ，該集合對介於兩者之間的真規則集均安全可行。若下包絡已不可行，則真規則集亦不可行；但「下包絡可行、上包絡不可行」不能決定真系統狀態。若上包絡最優值有限，額外採用安全上包絡解的成本，至多為 $\tau(R_U)-\tau(R_L)$ 。此處是確定性的集合包含界，不是信賴區間或統計不確定性。

6. 研究結果：算法交叉核查及幾何構造

6.1 香港初中幾何語義示例

考慮三角形 $ABC$ ，已知 $AB=AC$ ，點 $D$ 為邊 $BC$ 上的內點， $AD$ 平分頂角 $\angle BAC$ 。欲證明 $BD=DC$ 。本研究者按中學幾何基本定理人工構造兩種不同推論方法：

方法甲先引用 $AB=AC$ 、 $\angle BAD=\angle DAC$ 及共同邊 $AD=AD$ ，由 SAS 判定 $\triangle BAD\cong\triangle CAD$ ，其後由全等三角形對應邊相等導出 $BD=DC$ 。這一步的全等判定本身是一條包含多個前提的 AND 規則；若只有角相等，不能推出三角形全等。

方法乙由「 $AD$ 是內角平分線」及「 $D$ 位於 $BC$ 的內部」依角平分線定理推得 $BD/DC=AB/AC$ ，再結合 $AB=AC$ 得 $BD/DC=1$ ，即 $BD=DC$ 。這條推理使用了不同的中間命題「角平分線長度比例」，其正長度與位置前提不可省略。因此兩條完整推理同時存在時，若候選提示只允許選「SAS 全等」及「角平分線比例」，便須各命中一次，才能完全覆蓋所列兩條證明樹。

但如果教學規則庫允許直接援引「等腰三角形頂角平分線亦為底邊中線」，則可從已知直接導出 $BD=DC$ ，而不經上述兩個候選命題；本模型將正確判定在該擴充規則集下無有限提示截樹。故「是否列盡證明方法」、「何種定理可直接引用」乃邏輯模型中的重要約定。此幾何例子的數學論證可由讀者檢查，惟沒有香港教師對正式規則庫作獨立驗證，不應以本例宣稱已獲學校採用。

6.2 人工二分構造的成本與證書

二分構造有邊 $\{a,c\},\{a,d\},\{b,d\}$ ，費用 $c_a=2,c_b=3,c_c=2,c_d=1$ 。其全部 16 個候選集合可直接檢查： $\{a,d\}$ 費用 3； $\{c,d\}$ 亦費用 3，且兩者均覆蓋每條邊。最小割程序回傳 $\{a,d\}$ 及相同費用的最大流 3；獨立枚舉確認兩個同價解。這可作人工算法正確性的交叉核查，不能推論任何實際幾何題的提示成本相同。

6.3 更廣泛的人工驗證

表 3：解析結論與程式覆核的界線

人工情況	數學／程式結果	核驗方法	可以及不可以主張
$K_3$	整數 2；LP $3/2$	枚舉與限制求和證明	只能證明抽象整數差距
二分四節點	兩套最優集合；費用 3	Horn 閉包、獨立頂點覆蓋及等值流	子類內有限核查
260 組隨機 3+3 人工二分圖	全部 64 子集與最大流成本相符	固定種子獨立核查	不能代表任意圖之性能
240 組一般人工 Horn	每組 16 個集合之支撐集與閉包解相同	獨立有限樹支撐枚舉	不能證實大型真實證明情況
完整圖 $3\le n\le9$	整數最優 $n-1$	全枚舉；解析公式獨立證明	有限點不是一般證明的替代
成本 $x=0,1,\ldots,20$	$\min\{x+1,3\}$	流割與閉包窮舉	對全體實數 $x$ 仍靠解析推導
無規則、未可截的直接規則、零成本、無根循環	依次回報 0、不可行、0、不可導出	程式邊界檢查	不等於學生學習實驗

兩組人工隨機試驗合計 500 個小規模形式系統；其中一般 Horn 系統的四個合資格節點分別具有 16 種介入，而二分圖的六個合資格節點具有 64 種介入。確認的是兩種不同算法在已生成資料上的一致性。數學上的定理 1–5 依前面正式證明成立，不是藉試驗數量聲稱定理為真。上述實驗沒有變異數、效果量、顯著性或學生樣本數等統計推論。

7. 討論：形式提示覆蓋與教育有效性的差距

數學模型的第一個潛在用途是對規則正確性與可容許的證明方式作透明檢查。教師若建立限定題目的推理規則庫，便可藉最小閉包檢查一組候選提示能否覆蓋所有已記錄的證明樹。然而，規則庫一旦漏掉某個常見定理或混淆「必須同時成立」的條件，算法輸出仍可能在其錯誤語義下完全精確。因此課程及數學判準優先於演算法結果。

第二個用途是對最優性聲明進行分層審核。對二分構造，讀者有合法頂點覆蓋與同值最大流，可以核對最佳成本；對一般 Horn 模型，一份 LP 打包向量只提供下界。由完整圖 $K_n$ 的差距可見，在一般多前提系統中要求整數集合，不能把可行分數流量、局部樹流量或任意 LP 解直接當成最佳提示集合。

第三個用途是公開成本敏感度而非把數值費用神秘化。若教師使用主觀成本分級，式（11）的策略切換可以提示：不同成本假設可能改變最優集合，故應提供成本來源、同價替代方案和不確定性界。這只是模型內的條件分析；沒有證據顯示人工成本與學生認知負荷、性別、社經背景或考試表現有可測量關係。

Hein 與 Prediger（2024）研究的是證明中邏輯結構的圖像及語言支架，提供了未來如何設計真實教學研究的文獻線索；本文不借用該研究中的學生效果來填補香港資料空白。下一階段若要研究香港課室效果，應先由教師逐條審定題目規則及定理粒度，再採用倫理合規的學生資料蒐集、明確對照條件與適合的推斷方法；本稿沒有進行上述工作。

8. 限制及未來驗證

形式語義限制。 本研究採用正向、單調、單結論 Horn 推理，尚未納入反證法的暫時假設作用域、三角形退化情況、代數分母非零限制、存在量詞或測地／構圖證據。一個證明樹即使在語法上成立，也必須以數學與教師審查確認語義有效。

不完備規則限制。 定理 5 的包絡只在研究者能真正保證 $R_L\subseteq R_*\subseteq R_U$ 時才有保證；否則「最優上下界」是條件性結果。現有人工幾何示例只列出兩條方法，沒有證明已列盡一切合法證明。

最佳化及心理測量限制。 人工成本只是一種抽象非負數，無法驗證一個提示是否促進理解。把選提示視為刪除節點，只是在算法上檢查未提示推理是否存在，無法由此推導學生在真正獲提示後的學習行為。

數值驗證限制。 試驗中的 260+240 個小型系統、21 個成本格點與完整圖 $n\le9$ 是固定種子人工資料。它們不對軟件以外的數學模型語義作證，也不是形式定理證明、更不是香港學生樣本。

文獻及原創性限制。 研究模型與既有 Horn、超圖、最小 hitting set、axiom pinpointing、diagnosis、Vertex Cover 及最大流理論有明顯交集；未完全核閱付費論文全文或做系統文獻回顧，不能宣稱研究缺口已被徹底證實。仍需要外部學者與香港中學幾何教師審查。

9. 結論

本文把有限多前提幾何證明的「選一組與所有完整證明相交的提示點」明確表述為 Horn 閉包及證明樹支撐擊中集問題。已知 Vertex Cover 歸約顯示兩前提、無環系統亦可有 NP-complete 的最壞情況；一個具明確二分交互的兩層子類可借助經典流割理論得到整數最佳證書，而一般系統的分數打包只能給下界。完整圖的整數差距、成本敏感度與規則包絡進一步給出驗證輸出的合理界線。

本研究的學術定位是：把成熟組合最佳化定理、可核驗證書及香港初中幾何提示的受限邏輯語義作可重現的理論整合。 這些結果可供後續教師規則核查、設計嚴謹的幾何提示測試或開發教學研究假設，卻未對學生理解與教學成效作任何實證檢驗。

參考文獻

Bläsius, T., Friedrich, T., Lischeid, J., Meeks, K., & Schirneck, M. (2022). Efficiently enumerating hitting sets of hypergraphs arising in data profiling. Journal of Computer and System Sciences, 124, 192–213. https://doi.org/10.1016/j.jcss.2021.10.002

Gallo, G., Longo, G., Pallottino, S., & Nguyen, S. (1993). Directed hypergraphs and applications. Discrete Applied Mathematics, 42(2–3), 177–201. https://doi.org/10.1016/0166-218X(93)90045-P

Hein, K., & Prediger, S. (2024). Scaffolds for seeing, using, and articulating logical structures in proofs: Design research study with high school students. The Journal of Mathematical Behavior, 74, 101123. https://doi.org/10.1016/j.jmathb.2023.101123

Karp, R. M. (1972). Reducibility among combinatorial problems. In R. E. Miller & J. W. Thatcher (Eds.), Complexity of computer computations (pp. 85–103). Plenum Press. https://doi.org/10.1007/978-1-4684-2001-2_9

Peñaloza, R. (2020). Axiom pinpointing. In G. Cota, M. Daquino, & G. L. Pozzato (Eds.), Applications and practices in ontology design, extraction, and reasoning (Studies on the Semantic Web, Vol. 49, pp. 162–177). IOS Press. https://doi.org/10.3233/SSW200042

Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57–95. https://doi.org/10.1016/0004-3702(87)90062-2

Yao, S., Holzer, N., Santolucito, M. P., Ray, B., Jana, S., & She, D. (2026). Cost-efficient theorem proving via agent orchestration in program verification [Preprint]. arXiv. https://arxiv.org/abs/2610.09681

香港教育局。（2019）。《修訂中學數學課程介紹及初中演繹幾何的學與教》[教師專業發展研習簡報]。https://www.edb.gov.hk/en/curriculum-development/kla/ma/res/ss/handoutss.html

香港教育局。（2020）。《初中數學課程闡釋》。https://www.edb.gov.hk/attachment/tc/curriculum-development/kla/ma/curr/EN_KS3_tc.pdf