HOL Lightとは？

　話が前後しますが，HOL Lightの紹介です．
　私の学生時代の愛読書に『数学の基礎』（日本評論社）という島内剛一先生の労作があります．これは初等超越関数までを数理論理の手法により構成したもので，現在においても類書のない一冊だと思います．
　一方，計算機を用いて，この数理論理の手法により数学を構成する試みが，Automated Reasoning（自動推論）
http://en.wikipedia.org/wiki/Automated_reasoning
Automated Theorem Proving（自動定理証明）
Automated Deduction（自動演繹）
http://en.wikipedia.org/wiki/Automated_deduction
Formal methods（形式手法）などの名の下で
http://www.mcs.anl.gov/research/projects/AR/others.html
http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/0.html
http://www-formal.stanford.edu/clt/ARS/systems.html
http://www.ucalgary.ca/aslcle/logic-courseware
http://www.cs.ru.nl/~freek/100/index.html
http://www.cs.ru.nl/~freek/demos/
のように進められており，特に有名なのが，Isabelle/HOL
http://www.cl.cam.ac.uk/research/hvg/index.html
および，Mizar/QED Project
http://mizar.uwb.edu.pl/
http://mizar.org/qed/
です．
　前者は，証明全体を記述し読み込ませるタイプのシステム，後者は，証明内の処理（tactic）のコマンドを列挙するスタイルのLCF直系のシステムで，日本語で読める解説として，Isabellaについては
http://d.hatena.ne.jp/caeruiro/
Mizarについては，信州大の
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html
がありますが，HOLシリーズのHOL4
http://hol.sourceforge.net/
HOL Light
http://www.cl.cam.ac.uk/~jrh13/hol-light/
ProofPower
http://www.lemma-one.com/
についてはないようです．
　HOLシリーズの本家はHOL4ですが，こちらはどなたかにお任せするとして，このブログでは（プログラム検証などの生臭い話ではなく）数学を指向し，QEなども取り入れCASよりの立場ながら，トップクラスの証明能力を有するHOL Lightについて，気軽に読めるものを書いて行こう思っています．（影の声：Theoremaはどうした！）