Loading article…
プロトタイプ検証システム( PVS )は、カリフォルニア州メンロパークのSRI インターナショナルのコンピュータサイエンス研究所で開発された、サポートツールと自動定理証明器が統合された仕様言語です。
PVS は、依存型を持つチャーチの型理論の拡張からなるカーネルに基づいており、基本的には古典的な型付き高階論理です。基本型には、ユーザーが導入できる解釈されない型と、ブール値、整数、実数、順序数などの組み込み型が含まれます。型コンストラクタには、関数、セット、タプル、レコード、列挙、抽象データ型が含まれます。述語サブタイプと依存型を使用して制約を導入できます。これらの制約された型は、型チェック中に証明義務 (型の正確性条件または TCC と呼ばれる) を負う場合があります。PVS 仕様は、パラメータ化された理論に編成されています。
このシステムはCommon Lispで実装されており、GNU General Public License (GPL) に基づいてリリースされています。
参照
参考文献
外部リンク
- SRIインターナショナルのコンピュータサイエンス研究所のPVSウェブサイト
- マイケル・コールハースとキャロリン・タルコットの機械化推論データベースにおけるジョン・ラッシュビーによるPVSの要約