有些「單一公理」的代數 presentation，要從該公理推回一般的群律會極其困難 -- 比如 Division presentation 裡 Div→Group 需要證明 $\text{/-trans} : (a/c)/(b/c) = a/b$ ，但我們手上卻只有一個等式

x / (((x / x) / y / z) / (((x / x) / x) / z)) = y

這表示手算很難直接湊出來。不過我們可以靠自動定理證明器 OTTER（及其後繼者 Prover9）找出來

這裡記錄實際流程：先讓 Prover9 找出論證骨架，再逐條把它轉寫成 Agda 的等式推理。Prover9 能告訴我們「哪些中繼引理、用什麼順序、由誰推出誰」，剩下的就只是無聊的轉譯工作

安裝 [local-0]

macOS 上可以用 Homebrew，這會一併裝上找反例用的 mace4：

brew install prover9

把問題寫成輸入檔 [local-1]

Prover9 是一階等式邏輯的證明器。用 op(...) 宣告二元運算，公理要寫成 assumptions，要證的目標放進 goals（Prover9 實際上是去否證目標的反例）。以 Higman–Neumann 單一除法公理證 /-trans 為例，存成 trans.in：

op(400, infix, "/").

formulas(assumptions).
  % Higman–Neumann
  x / ((((x / x) / y) / z) / (((x / x) / x) / z)) = y.
end_of_list.

formulas(goals).
  (a / c) / (b / c) = a / b.
end_of_list.

接著跑，看有沒有證出來，並把證明物件抓出來：

prover9 -f trans.in > trans.out
grep "THEOREM PROVED" trans.out
sed -n '/=* PROOF =*/,/=* end of proof =*/p' trans.out

可以用 assign(max_seconds, 30). 設搜尋時限；找反例（證明某式「不」成立）則改用 mace4 -f model.in

把長證明拆成「好轉寫」的小引理 [local-2]

如果嘗試直接證 /-trans 會得到一條約 30 步、項非常巨大的 paramodulation 結果，幾乎沒辦法使用。關鍵技巧是把已經證好的中繼引理當成額外 assumption 餵回去，每一步只讓 Prover9 補幾步，產生的子句就短到能逐條轉寫

Division presentation 做的大致上依序是：

RID： $x/(y/y) = x$ （右單位）
UNIT： $x/x = y/y$ （單位唯一）
INVL： $(x/x)/((x/x)/y) = y$ （逆元對合）
CL47： $(x/y)/((z/z)/y) = x$ （右消去）
CL8：公理對自己代入得到的橋梁等式
FLIP： $(x/x)/(y/z) = z/y$ （翻轉）
/-trans： $(a/c)/(b/c) = a/b$ （master lemma）

每證好一條就把它加進下一個輸入檔的 assumptions，於是「Prover9 證下一條」的搜尋只剩幾步

把子句轉寫成 Agda [local-3]

Prover9 證明裡每條子句長這樣：

102 x / (y / y) = x.  [para(2(a,1),5(a,1,2,2))]

方括號是「這條怎麼來的」。para(p,q) 是把子句 p 的等式代入並改寫子句 q 的某個子項；rewrite([k(..)]) 是再用引理 k 改寫一次。對應到 Agda，一條子句就是一段 _＝⟨_⟩_ 鏈：para 是代入特定值後套用某條等式，rewrite 則是 ap (λ w → …) (lemma …) 改寫子項

看懂 para 裡的位置標記很有幫助：7(a,1,1) 表示「子句 7、等式左邊（1）、它的第一個引數（1）」。把位置對上要改寫的子項，就能還原 Prover9 用的代入，再照子句的相依順序逐條寫成 Agda，最後用 agda 檢查通過即可