PVSのこと（０）

　と言うわけで，暫くは PVS のことを書きます．

PVS はSRI(スタンフォード)で90年代初めより開発が進められている対話的定理証明システムで，LK が素直にインプリメントされており論理記号の消去は極めて平易に行えるのですが，ground，grind，assertといった簡約コマンドはあるものの，mesonやmetisのようなFOLプルーバーは実装されておらず，同じSRI製のSMTであるYicesでは，HOL系のシステムと比べるともどかしさがあります．しかし，ラングレーフォーマルメソッドグループ(NASA)の手になるライブラリーはかなり充実しており，数学科の学部程度の内容を網羅，ルベーグ積分だけでなくリーマン積分も含まれています（ゲージ積分はありません（笑））．また，同グループによる数式のマジックハンド的な変形ストラテジー群Manipも逐次取り入れた結果，Prototype Verification System という名前とは裏腹に，非常に数学向きのシステムとなっています．