ヴァンパイア（定理証明器）

ヴァンパイアは、マンチェスター大学のコンピュータサイエンス学部で開発された、一階古典論理の自動定理証明器である。バージョン3までは、アンドレイ・ヴォロンコフがクリシュトフ・ホダーと共同で開発し、それ以前はアレクサンドル・リアザノフと共同で開発していた。バージョン4以降は、ローラ・コヴァックス、ジャイルズ・レガー、マーティン・スーダを含む幅広い国際チームが開発に携わっている。1999年以来、ヴァンパイアは「定理証明器の世界カップ」であるCADE ATPシステムコンペティションで少なくとも53のトロフィーを獲得しており、その中には最も権威のあるFOF部門と理論推論TFA部門も含まれている。^{[3] [4]}

Vampire のカーネルは、順序付きバイナリ解決と重ね合わせ(等式の処理)の計算を実装します。分割規則と負の等式分割は、新しい述語定義の導入とそのような定義の動的折りたたみによってシミュレートできます。DPLLスタイルのアルゴリズム分割もサポートされています。検索空間の刈り込みには、 トートロジー削除、包含解決、順序付き単位等式による書き換え、基本性制限、置換項の既約性など、いくつかの標準的な冗長性基準と簡略化手法が使用されます。項の削減順序は、標準のKnuth–Bendix 順序です。

用語と句のセットに対するすべての主要な操作を実装するために、いくつかの効率的なインデックス作成手法が使用されます。実行時アルゴリズムの特殊化は、前方一致を高速化するために使用されます。

システムのカーネルは連言正規形のみで動作しますが、プリプロセッサ コンポーネントは完全な 1 階論理構文で問題を受け取り、それを句化し、いくつかの有用な変換を実行してから結果をカーネルに渡します。定理が証明されると、システムは検証可能な証明を生成し、句化フェーズと連言正規形の反証の両方を検証します。

定理の証明に加えて、Vampire には補間の生成などの他の関連機能もあります。

実行ファイルはシステムのウェブサイトから入手できます。^[5] 2020年11月現在、VampireはBSD 3条項ライセンスの修正版の下でリリースされており、商用利用が明示的に許可されています。以前のバージョンは、独自の非商用ライセンスの下で利用可能でした。

• 公式サイト