provers on HOL Light
proverには担当分野があります．例えば
# MESON[] `1+2=1+2`;;
0..0..solved at 2
val it : thm = |- 1 + 2 = 1 + 2
は処理できても
# MESON[] `1+2=2+1`;;
0..0..1..2..6..11..19..30..41..54..81..108..149..214..279..368..489..610..763..9
96..1229..1542..1923..2304..2753..3338..3923..4644..5591..6538..7711..9132..1055
3..12222..14397..16572..19253..22714..26175..30416..35633..40850..47043..55268..
63493..73750..87057..100364..116721..137866..159011..Exception: Failure "solve_g
oal: Too deep".
のようになります．この違いは前者は，等式の両辺が同じ式であり，これは等号の公理に含まれるのに対して，後者では，両辺を計算した結果が等しいだけで，論理式としては異なりますから，等号の公理は知っていても＋についての知識を持たないMESONには処理できないわけです．そこで，＋という２変数関数についての対称性の定理
# ADD_SYM;;
val it : thm = |- !m n. m + n = n + m
を仮定としてMESONに与えると
# MESON[ADD_SYM]`1+2=2+1`;;
0..0..solved at 2
val it : thm = |- 1 + 2 = 2 + 1
のように証明可能と答えてくれます．
しかし，計算にはそれを担当するprover関数が幾つも用意されています．
HOL Lightは，数学を公理的に構成していますので，数の体系も
(num)自然数
(int)整数
(real)実数
(complex)複素数
の順に拡張され，proverも扱う数の範囲毎に存在するだけでなく，パッケージをロードすれば，コアとは異なるアルゴリズムを用いて，より複雑な定理を証明することも出来ます．具体的にはデフォルトの
ARITH_RULE for num
INT_ARITH for int
REAL_ARITH for realNUM_RING
INT_RINGREAL_FIELD
そして，cooper.mlを
#use "Examples/cooper.ml";;
のようにロードすれば使える
COOPER_RULE for num
INT_COOPER for int
或いは，先日述べたcsdpをパスの通ったところにインストールし
#use "Examples/sos.ml";;
のようにロードすれば使える
SOS_RULE for num
INT_SOS for int
REAL_SOS for real
などがあります．
