| 翻訳と辞書 |
Nuprl
Nuprl is a proof development system, providing computer-mediated analysis and proofs of formal mathematical statements, and tools for software verification and optimization. Originally developed in the 1980s by Robert Lee Constable and others, the system is now maintained by the PRL Project at Cornell University. The currently supported version, Nuprl 5, is also known as FDL (Formal Digital Library). Nuprl functions as an automated theorem proving system and can also be used to provide proof assistance.
== Design ==
Nuprl uses a type system based on Martin-Löf intuitionistic type theory to model mathematical statements in a digital library. Mathematical theories can be constructed and analyzed with a variety of editors, including a graphical user interface, a web-based editor, and an Emacs mode. A variety of evaluators and inference engines can operate on the statements in the library. Translators also allow statements to be manipulated with Java and OCaml programs.〔(【引用サイトリンク】url=http://www.nuprl.org/images/FDL-diagram.png )〕 The overall system is controlled with a variant of ML.
Nuprl 5 is intended primarily to be used as a web service rather than as standalone software. Those interested in using the web service, or migrating theories from older versions of Nuprl, can contact the email address given on the Nuprl System web page.〔(【引用サイトリンク】url=http://www.nuprl.org/html/NuprlSystem.html )〕
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「Nuprl」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|