数学/Proof Checker

数学の証明正誤判断器(proof checker)にはバッチ型と対話型がある。

型	言語	種類
バッチ型	構造化された証明記述言語	Automath, CAP, Mizar, PX, ...
対話型	スクリプト言語	Boomborg-PC, Coq, EKL, ELF, EUODHILOS-II, FOL, HOL, IMPS, Isabelle, LCF, Lego, Nuprl, NQTHM, PVS, ...