PVS の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• PVS へ行く。

*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