![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
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 が開発，公開している対話的定理証明システムです．その特徴は
といった基本性能と
との融合，つまり，簡明な推論規則と多様な既知事項の運用により，述語論理のプルーバーを持たないにも拘わらず，ケンブリッジ 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 ./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 版のインストール例はこちらです．
起動
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
で証明が表示されます．
