PVS
の編集
http://ftp.mathlibre.org/wiki/?PVS
[
トップ
] [
編集
|
差分
|
バックアップ
|
添付
|
リロード
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
-- 雛形とするページ --
(no template pages)
*PVS + NASA PVS Library [#l933018e] The PVS (Prototype Verification System) is a comprehensive verification environment: it provides a specification language in which mathematical theories and conjectures can be specified, together with an interactive theorem prover. The PVS specification language is a higher-order logic with a rich type system that supports concise and perspicuous specifications. Its theorem prover provides powerful automation, with decision procedures for several theories including real and integer arithmetic. PVS は SRI International の Computer Science Laboratory が開発,公開している対話的定理証明システムです.その特徴は - シークエント計算(LK)に基づく論理体系 - 高度な自動代数処理 - 入力コストを抑えた証明スクリプト作成環境(emacs) といった基本性能と - NASA Langley Formal Methods Team 提供による膨大かつマニアックなライブラリー : http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/library.html との融合,つまり,簡明な推論規則と多様な既知事項の運用により,述語論理のプルーバーを持たないにも拘わらず,ケンブリッジ HOL シリーズと同等の定理を証明できる点にあります. *インストール例 [#x6ddfc68] NASA Library を含めたインストールには約1.2ギガの空きスペースが必要です.なお,商用の Allegro Lisp 版には(ワンクリックですが)利用承認が必要なので,今回は低速ながらオープンの SBCL 版を用います(検索ツール Hypatheon は Allegro 版のみのサポートです). sudo apt-get -y install sqlite3 echo "export PVS_LIBRARY_PATH=/usr/local/CAS/pvs6/nasalib" >> ~/.bashrc source ~/.bashrc export CAS=/usr/local/CAS sudo mkdir $CAS sudo mkdir $CAS/pvs6 cd $CAS/pvs6 sudo chmod -R 777 $CAS wget http://pvs.csl.sri.com/download-open/pvs-6.0-ix86_64-Linux-sbclisp.tgz tar zxvf ./pvs-6.0-ix86_64-Linux-sbclisp.tgz rm ./pvs-6.0-ix86_64-Linux-sbclisp.tgz ./bin/relocate sudo ln -s $CAS/pvs6/pvs /usr/local/bin/pvs-sbcl wget http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/nasalib-6.0.6-full.tgz tar xvfz ./nasalib-6.0.6-full.tgz rm ./nasalib-6.0.6-full.tgz Allegro Lisp 版のインストール例はこちらです. - http://d.hatena.ne.jp/ehito/20130925/1380080475 *使用例 [#laa0e3fe] - http://d.hatena.ne.jp/ehito/20130624/1372076440 起動 pvs-sbcl ./demo.pvs 次をコピペ demo1:theory begin importing reals@sigma[posnat] lem1:lemma FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) end demo1 カーソルを lem1 の上に置いて M-x pr Rule? と表示されたら Tab C-s Variable on which to induct-and-simplify: と表示されたら n と入力後,デフォルトで数回エンター.Rule? と表示されたら Tab r Replace using formula: と表示されたら -1 と入力後,デフォルトで数回エンター.Rule? と表示されたら (grind-reals) とすれば証明完了. M-x show-last-proof で証明が表示されます. *リンク [#odd5ad71] - http://pvs.csl.sri.com/index.shtml - http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/ - http://ocvs.cfv.jp/tr-data/ps05-009.pdf - http://d.hatena.ne.jp/ehito/20130624/1372036887 - http://www.youtube.com/watch?v=kzGdyRruGo8 - http://www.youtube.com/watch?v=H3-qtqrjUiM
タイムスタンプを変更しない
*PVS + NASA PVS Library [#l933018e] The PVS (Prototype Verification System) is a comprehensive verification environment: it provides a specification language in which mathematical theories and conjectures can be specified, together with an interactive theorem prover. The PVS specification language is a higher-order logic with a rich type system that supports concise and perspicuous specifications. Its theorem prover provides powerful automation, with decision procedures for several theories including real and integer arithmetic. PVS は SRI International の Computer Science Laboratory が開発,公開している対話的定理証明システムです.その特徴は - シークエント計算(LK)に基づく論理体系 - 高度な自動代数処理 - 入力コストを抑えた証明スクリプト作成環境(emacs) といった基本性能と - NASA Langley Formal Methods Team 提供による膨大かつマニアックなライブラリー : http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/library.html との融合,つまり,簡明な推論規則と多様な既知事項の運用により,述語論理のプルーバーを持たないにも拘わらず,ケンブリッジ HOL シリーズと同等の定理を証明できる点にあります. *インストール例 [#x6ddfc68] NASA Library を含めたインストールには約1.2ギガの空きスペースが必要です.なお,商用の Allegro Lisp 版には(ワンクリックですが)利用承認が必要なので,今回は低速ながらオープンの SBCL 版を用います(検索ツール Hypatheon は Allegro 版のみのサポートです). sudo apt-get -y install sqlite3 echo "export PVS_LIBRARY_PATH=/usr/local/CAS/pvs6/nasalib" >> ~/.bashrc source ~/.bashrc export CAS=/usr/local/CAS sudo mkdir $CAS sudo mkdir $CAS/pvs6 cd $CAS/pvs6 sudo chmod -R 777 $CAS wget http://pvs.csl.sri.com/download-open/pvs-6.0-ix86_64-Linux-sbclisp.tgz tar zxvf ./pvs-6.0-ix86_64-Linux-sbclisp.tgz rm ./pvs-6.0-ix86_64-Linux-sbclisp.tgz ./bin/relocate sudo ln -s $CAS/pvs6/pvs /usr/local/bin/pvs-sbcl wget http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/nasalib-6.0.6-full.tgz tar xvfz ./nasalib-6.0.6-full.tgz rm ./nasalib-6.0.6-full.tgz Allegro Lisp 版のインストール例はこちらです. - http://d.hatena.ne.jp/ehito/20130925/1380080475 *使用例 [#laa0e3fe] - http://d.hatena.ne.jp/ehito/20130624/1372076440 起動 pvs-sbcl ./demo.pvs 次をコピペ demo1:theory begin importing reals@sigma[posnat] lem1:lemma FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) end demo1 カーソルを lem1 の上に置いて M-x pr Rule? と表示されたら Tab C-s Variable on which to induct-and-simplify: と表示されたら n と入力後,デフォルトで数回エンター.Rule? と表示されたら Tab r Replace using formula: と表示されたら -1 と入力後,デフォルトで数回エンター.Rule? と表示されたら (grind-reals) とすれば証明完了. M-x show-last-proof で証明が表示されます. *リンク [#odd5ad71] - http://pvs.csl.sri.com/index.shtml - http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/ - http://ocvs.cfv.jp/tr-data/ps05-009.pdf - http://d.hatena.ne.jp/ehito/20130624/1372036887 - http://www.youtube.com/watch?v=kzGdyRruGo8 - http://www.youtube.com/watch?v=H3-qtqrjUiM
テキスト整形のルールを表示する