数学/Proof Checker

出典: フリー教科書『ウィキブックス(Wikibooks)』
ナビゲーションに移動 検索に移動

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

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