MESONは非常に優秀なproverであり，例えば # let lemma = `!x:real. ?n:num. &1 <= x ==> &1 <= &n /\ floor x = &n`;; val lemma : term = `!x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n`の証明に必要な # [FLOOR; integer; ABS_REFL; REAL_LE_FLOOR; INT…

既出の本家筋以外は中々見当たらないのですが，次の論文の補足Ｂに入門的な解説があります． http://rudar.ruc.dk/bitstream/1800/6890/1/8%20-%20Automatization%20of%20the%20semantic%20tableau%20method.pdf なお，取り上げられている例をただ証明するだ…

ご覧のように，HOL Light は，数学科の学部程度の定理(Pre-proved Theorems)とそれを用いて新たな定理の証明を作成する為の関数(Pre-de ned ML Identi ers)からなる，所謂，proof assistantですが，MizarやCoqよりも知名度が低いように思えます．その理由の…