ほとんどの証明アシスタントは、従属型を持つ関数型プログラミング言語です。プログラム/アルゴリズムを証明できます。代わりに、数学のみに最適な証明アシスタント (たとえば微積分) に興味があります。1つお勧めできますか？Mizar について聞いたことがありますが、ソース コードが閉じられているのは好きではありませんが、数学に最適な場合は使用します。Agda や Idris などの新しい言語は、数学的な証明にどの程度適していますか?
質問する
905 次
1 に答える
12
Coq実際の分析をカバーする広範なライブラリがあります。さまざまな展開が思い浮かびます。
標準ライブラリと、現在は機能していないcoqtailプロジェクト [1] (ベキ級数を幅広くカバーし、複素数に関するかなりの作業がある) や、より最近のcoquelicotなど、その上に構築されているプロジェクト。これらはすべて、ここで提示される実数の公理的な定義に依存しています。
より建設的なアプローチは、実物を実際に構築することから始まるC-CoRNプロジェクトによって提供されます。
実数に取り組むもう 1 つの方法は、非標準的な分析に目を向けることです。これは、使用しACL2ている人々が行ってきたことです。
この分野のより一般的な見方については、おそらく、coquelicot プロジェクトに関係する人々によるこの調査論文を読む必要があります。
[1] 完全な開示: 私はそのプロジェクトに関わっていました
于 2015-02-16T14:37:48.380 に答える