HOL Light の位置付け
ご覧のように，HOL Light は，数学科の学部程度の定理(Pre-proved Theorems)とそれを用いて新たな定理の証明を作成する為の関数(Pre-de ned ML Identi ers)からなる，所謂，proof assistantですが，MizarやCoqよりも知名度が低いように思えます．その理由の一つは，Mizarから見るとコンピュータよりであり，Coqから見ると数学よりであるという点かも知れません．
ご覧のように，HOL Light は，数学科の学部程度の定理(Pre-proved Theorems)とそれを用いて新たな定理の証明を作成する為の関数(Pre-de ned ML Identi ers)からなる，所謂，proof assistantですが，MizarやCoqよりも知名度が低いように思えます．その理由の一つは，Mizarから見るとコンピュータよりであり，Coqから見ると数学よりであるという点かも知れません．