オートマス

Automath（「数学の自動化」）は、1967 年にNicolaas Govert de Bruijnによって考案された形式言語であり、組み込まれた自動証明チェッカーが理論の正確性を検証できるような方法で完全な数学理論を表現するために使用されます。

概要

オートマスシステムには、後に型付きラムダ計算や明示的置換といった分野で採用・再発明される多くの斬新な概念が含まれていました。依存型はその顕著な例の一つです。オートマスはまた、カリー・ハワード対応を活用した最初の実用的なシステムでもありました。命題は証明の集合（「カテゴリー」と呼ばれる）として表現され、証明可能性の問題は非空性（型の居住）の問題となりました。デ・ブリュインはハワードの研究を知らず、独自に対応を述べました。^{[ 1 ]}

LS van Benthem Jutting は、1976 年の博士論文の一環として、Edmund LandauのFoundations of Analysis をAutomath に翻訳し、その正確性を確認しました。

しかし、オートマスは当時広く宣伝されることはなく、広く使用されることはなかった。しかし、その後の論理フレームワークや証明支援システムの発展に大きな影響を与えた。^{[ 2 ] [ 3 ]}形式化された数学を記述および検証するシステムであり、現在でも使用されているミザールシステムは、オートマスの影響を受けている。

参照

• QEDマニフェスト

参考文献

1. Morten Heine Sørensen、Paweł Urzyczyn、 Curry-Howard 同型性に関する講義、エルゼビア、2006、 ISBN 0-444-52077-5、98-99ページ
2. RP Nederpelt、JH Geuvers、RC de Vrijer (1994) Automath に関する厳選論文。 Vol. 133 of Studies Logic、エルゼビア、アムステルダム。 ISBN 0-444-89822-0。
3. F. Kamareddine (2003)数学の自動化35年ワークショップ、ドルドレヒト、ボストン、Kluwer Academic Publishers発行、 ISBN 1-4020-1656-5。

外部リンク

• オートマスアーカイブ（ミラー）
• Automathの35周年を祝うワークショップのホームページ
• Freek Wiedijk によるAutomath ページ