自動定理証明

　現在の定理証明プログラムは
・論理式を入力すれば，自動的に証明してくれる（ものによっては証明も出力する），いわゆる，prover．
例）otter/prover9
http://www.mcs.anl.gov/research/projects/AR/otter/index.html
http://www.cs.unm.edu/~mccune/mace4/
SPASS
http://www.spass-prover.org/
そして，Theorema
http://www.risc.jku.at/research/theorema/description/
・証明に用いる定理や規則を対話的に入力する，いわゆる，proof assistant．
例）LCF
http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/lcf/0.html
Nqthm
http://www.computationallogic.com/software/nqthm/index.html
PVS
http://pvs.csl.sri.com/
Coq
http://coq.inria.fr/
・証明全体を入力すれば，その正しさを検証してくれる，いわゆる，proof checker．
例）Mizar
http://mizar.uwb.edu.pl/

の３つに大別できます．当然ですが，自動化の度合いと扱える定理のレベルとは相反する要求であり，手放しで証明できるのは，比較的少ない前提で扱えるもののみと言って良く，それなりの内容の証明には，相応の人間の入力が必要となります．
　HOL Lightは，proof assistantであり，様々なtacticと呼ばれる指示を適宜入力して証明を完成させるタイプですが，簡単な処理を自動的に実行する関数も装備しており，しかも，同様の機能を備えたproof assistantより，その「簡単な処理」の水準が極めて高いことが特徴になっています．
　前回のMESONは，その中で等号を含む１階述語論理のproverで

# MESON[] `(~p ==> q /\ ~q) ==>p`;;
val it : thm = |- (~p ==> q /\ ~q) ==> p

のような命題論理の定理は勿論

# MESON[]`!x y a b. x=a /\ y=b /\ p(x,x) ==> f(x,y)=f(a,b) /\ ?z. p(x,z)`;;
Warning: inventing type variables
0..0..solved at 2
0..0..solved at 2
val it : thm =
　|- !x y a b.
　　　　x = a /\ y = b /\ p (x,x) ==> f (x,y) = f (a,b) /\ (?z. p (x,z))

のような関数，述語を含んだ定理まで自動的に証明してくれます．