Loading article…
オートマトン（「数学の自動化」の意）は、1967年にニコラース・ゴバート・デ・ブルインによって考案された形式言語であり、完全な数学理論を、内蔵された自動証明チェッカーがその正しさを検証できるような形で表現するためのものである。
Automath システムには、後に型付きラムダ計算や明示的置換などの分野で採用または再発明された多くの斬新な概念が含まれていました。依存型はその顕著な例の 1 つです。Automath はまた、Curry-Howard 対応を利用した最初の実用的なシステムでもありました。命題は証明の集合 (「カテゴリ」と呼ばれる) として表現され、証明可能性の問題は非空性 (型の占有)の問題になりました。de Bruijn は Howard の研究を知らず、独自に対応を述べました。[ 1 ]
L.S.ファン・ベンテム・ユッティングは、1976年の博士論文の一環として、エドムント・ランダウの『解析学の基礎』をオートマトンに翻訳し、その正確性を検証した。
しかし、Automathは当時広く宣伝されることはなく、広く普及することはありませんでしたが、後の論理フレームワークや証明支援システムの開発に非常に大きな影響を与えました。[ 2 ] [ 3 ]現在も活発に使用されている形式化された数学の記述と検証システムであるMizarシステムは、Automathの影響を受けています。