Loading article…
Nuprlは、形式的な数学的命題のコンピュータによる解析と証明、およびソフトウェアの検証と最適化のためのツールを提供する証明開発システムです。元々は1980年代にロバート・リー・コンスタブルらが開発したもので、現在はコーネル大学のPRLプロジェクトによって維持されています。現在サポートされているバージョンであるNuprl 5は、FDL（Formal Digital Library）としても知られています。Nuprlは自動定理証明システムとして機能するだけでなく、証明支援にも利用できます。
Nuprl は、Martin-Löf直観型理論に基づく型システムを使用して、デジタルライブラリで数学的ステートメントをモデル化します。数学理論は、グラフィカルユーザーインターフェース、Web ベースのエディタ、Emacsモードなど、さまざまなエディタを使用して構築および分析できます。さまざまな評価ツールと推論エンジンがライブラリ内のステートメントに対して操作できます。トランスレータを使用すると、ステートメントをJavaおよびOCamlプログラムで操作することもできます。[ 1 ] システム全体はMLのバリアントで制御されます。
Nuprl 5のアーキテクチャは「分散オープンアーキテクチャ」[ 1 ]と説明されており、Nuprl 5はスタンドアロンソフトウェアとしてではなく、主にWebサービスとして使用されることを目的としています。
Nuprl は 1984 年に初めてリリースされ、1986 年に出版された書籍「Implementing Mathematics with the Nuprl Proof Development System」[ 2 ]で初めて詳細に説明されました。Nuprl 2 は最初のUnixバージョンでした。Nuprl 3 は、ジラールのパラドックスとヒグマンの補題に関連する数学的問題の機械証明を提供しました。ワールド ワイド ウェブ向けに開発された最初のバージョンである Nuprl 4 は、キャッシュ コヒーレンシ プロトコルやその他のコンピュータ システムの検証に使用されました。[ 3 ]
Nuprl 5 で実装されている現在のシステム アーキテクチャは、2000 年の会議論文で初めて提案されました。Nuprl 5 のリファレンス マニュアルは 2002 年に発行されました。[ 4 ] Nuprl は、多くのコンピュータ サイエンス関連の出版物 の対象となっています。
JonPRLとRedPRLの両システムは、計算型理論に基づいている。[ 5 ] RedPRLは明確に「Nuprlに触発された」ものである。[ 6 ]