PVS + NASA PVS Library

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)


との融合,つまり,簡明な推論規則と多様な既知事項の運用により,述語論理のプルーバーを持たないにも拘わらず,ケンブリッジ HOL シリーズと同等の定理を証明できる点にあります.


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
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 版のインストール例はこちらです.



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: と表示されたら


と入力後,デフォルトで数回エンター.Rule? と表示されたら

Tab r

Replace using formula: と表示されたら


と入力後,デフォルトで数回エンター.Rule? と表示されたら



M-x show-last-proof



トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2015-01-09 (金) 18:44:24 (2519d)