1樓：
其實在 src tree 裡 grep 一下哪些地方用到了 aiLib 就可以知道這是啥了
嚒，其實就是用 AI 演算法指導 proof search。
因為新版本的 z3 不支援 tptp 格式就沒試
找了個 4.0.0 的 z3 試了下
> val kleene62 = ``~(A /\ B) <=> (~A \/ ~B)``;
val kleene62 = 「(A ∧ B) A ∨ B」: term
> holyhammer kleene62;
Loading 3105 theorems
proof found by z3:
metisTools.METIS_TAC
minimized proof:
METIS_TAC
metis: r[+0+4]#
val it = (A ∧ B) A ∨ B: thm
適用性一般複雜點的比如
> val kleene92 = ``(A \/ (!x. B x)) <=> !x. (A \/ B x)``;
<>val kleene92 = 「A ∨ (x. B x) x. A ∨ B x」: term
> holyhammer kleene92;
Loading 3105 theorems
Exception-
HOL_ERR
raised
就 timeout 了。
換了 vampire 試了下發現估計是 z3 的鍋。很快就能出來了，說明其實主要還是 SMT solver 在幹累活。不過這還是乙個非常有意思的相對不需要計算力的 ML 應用。
> val kleene92 = ``(A \/ (!x. B x)) <=> !x. (A \/ B x)``;
<>val kleene92 = 「A ∨ (x. B x) x. A ∨ B x」: term
> holyhammer kleene92;
Loading 3106 theorems
proof found by vampire:
metisTools.METIS_TAC
minimized proof:
METIS_TAC
metis: r[+0+4]#
r[+0+4]#
r[+0+3]#
val it = A ∨ (x. B x) x. A ∨ B x: thm
number theory 也可以
> holyhammer ``1 + 1 = 2``;
Loading 3106 theorems
proof found by vampire:
metisTools.METIS_TAC [arithmeticTheory.ALT_ZERO , arithmeticTheory.
SUC_ONE_ADD , arithmeticTheory.TWO , numeralTheory.numeral_distrib , numeralTheory.
numeral_suc]
minimized proof:
METIS_TAC [arithmeticTheory.SUC_ONE_ADD, numeralTheory.numeral_distrib, numeralTheory.
numeral_suc]
metis: r[+0+54]+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+0+1+1+0+0+1+1+3+2+6+6+8+9+7+0+2+0+1+6+0+2+2+3+0+3+0+2+3+2+3+0+2+2+3+0+2+4+5+0+4+4+5+0+4+5+5+23+22+22+6+0+2+0+1+2+37+36+19#
val it = 1 + 1 = 2: thm
> val indthm = ``!p.(p ZERO /\ !x. (p x ==> p (SUC x))) ==> !x.p x``;
val indthm = 「p. p ZERO ∧ (x. p x p (SUC x)) x. p x」: term
> holyhammer indthm;
Loading 3106 theorems
proof found by vampire:
metisTools.METIS_TAC [arithmeticTheory.ALT_ZERO , arithmeticTheory.
NOT_LESS , boolTheory.EQ_CLAUSES , numTheory.INDUCTION]
minimized proof:
METIS_TAC [arithmeticTheory.ALT_ZERO, numTheory.INDUCTION]
metis: r[+0+11]+0+0+1+0+0+0+0+0+0+1+2#
val it = p. p ZERO ∧ (x. p x p (SUC x)) x. p x: thm
ps. macOS 沒有 coreutils 的 timeout 。想想不如用 ATS 寫乙個。
2樓：
並沒有實際使用過這個功能…不過作為 Neuro-symbolic 的乙個方向，用 ML/DL 來做 HOL 定理證明的工作最近蠻多的， ICLR '17 有 HOLStep （https://
arxiv.org/pdf/1703.00426.pdf
），ICML '19 有 HOList （https://arxiv.org/pdf/1904.03241.pdf
），還有通過ML來為Isabelle/HOL選擇lemma的 （https://
people.mpi-inf.mpg.de/~jblanche/mash2.pdf
）。類似的工作在 Mizar/FOL/SMT/SAT 上也有不少，比如用MCTS 輔助 mlCoP FOL solver 證明（NIPS 18）、使用神經網路來學習SMT solver的求解策略（NIPS 18）、single bit supervised的純NN SAT Solver。
ERP是什麼東西？
西安安泰電子 ERP Enterprise Resource Planning 系統即企業資源計畫系統，含義是指建立在資訊科技基礎上，以系統化的管理思想，為企業決策層及員工提供決策執行手段的管理平台。一套好的ERP系統正是協助企業做好內控與提高管理效率的關鍵，目前ERP系統這一塊，智邦國際做的還是可...
密位是什麼東西？
陳傑亮 可看到附圖的分劃裡，乙個密位點大約等於0.2密位，每個點之間相距0.8密位 點到點為1密位 圖二則是三種標準的密位分劃，可以看到最右邊的二代改良版在點跟點之間刻有0.5密位的線，一來增加了乙個瞄準點，二來可以方便人們在腦海裡分成10等分。另一種密位型態則是如圖三這種斜線式的分劃 以下的線則是...
水離子是什麼東西？
永遠的蕭十一 所謂離子水，即通過淨水器利用活性炭作為過濾層，過濾自來水，使之淨化達標 達到國家級水標準 再通過膈膜電解生成兩種活性的水，即離子水。集中於陰極流出來的為鹼性離子水 供飲用 集中於陽極流出來的為酸性離子水 供外用 離子水不包括生理鹽水等新增有其他物質的水 者也 這就是一些商家的噱頭，水由...