Computing Witnesses Using the SCAN Algorithm

Fabian Achammer、Stefan Hetzl、および Renate A. Schmidt による論文「Computing Witnesses Using the SCAN Algorithm」の詳細な技術的概要を以下に示す。

1. 問題定義

本論文は、与えられた第二階論理式 $\exists X \phi$（ここで $\phi$ は第一階論理式）に対して、論理的に等価な第一階論理式 $\psi$ を見つける問題である**第二階量化子除去（SOQE）**を取り扱っている。SOQE は一般的には決定不能であるが、特定の部分クラスに対しては実用的なアルゴリズムが存在する。

著者らは、**Witnessed Second-Order Quantifier Elimination（WSOQE）**と呼ばれるより一般的な問題を導入する。単に等価な第一階論理式を見つけるだけでなく、witness（証人）、すなわち第一階述語の組 $\alpha$ を見つけることを目的とする。
$$\exists X \phi \equiv \phi[X \leftarrow \alpha]$$
これは、第二階論理式が、述語変数 $X$ を特定の第一階定義 $\alpha$ に置換して得られる第一階論理式と等価であることを意味する。

WSOQE の意義:

• SOQE と論理式方程式（FEQ）（$\models \phi[X \leftarrow \alpha]$ となる $\alpha$ を見つけること）の間のギャップを埋める。
• 知識表現（忘却/射影）、モダリティ対応理論、およびプログラム検証（ループ不変式の発見）における応用において重要である。
• 結果のみを生成する標準的な SOQE と異なり、WSOQE は除去された述語の定義を提供し、知識ベースの構造を保持する。

2. 手法：WSCAN アルゴリズム

著者らは、既存のSCAN アルゴリズム（SOQE 用の飽和ベースの定理証明器）を拡張したWSCANを提案する。核心的な手法は以下の 2 つの主要フェーズからなる。

A. SCAN 導出

このアルゴリズムは節集合上で動作する。入力論理式を節標準形に変換し、特定の推論計算 $\mathcal{I}$ を用いて飽和プロセスを実行する。

1. 制約解決と因数分解: 標準的な統一の代わりに、これらの規則は項間の不等式制約（例：$t \not\simeq t'$）を導入する。
2. 制約除去: 項を統一して制約を除去する。
3. 削除規則:
   • 拡張純粋性削除: $X$ が単一の極性（すべて正またはすべて負）でしか現れない場合、$X$ を含む節を除去する。
   • 精製節削除: 「十分に多くの」推論が実行され、残りの節集合が節 $P$ の解決閉包を論理的に含意する場合、$X$ を含む節 $P$ を除去する。これは変数除去と包含関係を含む前方冗長性基準を通じて形式化される。

このプロセスは、すべての $X$ 文字列が除去されるまで継続され、$\exists X N$ と等価な第一階節集合 $N^*$ が得られる。

B. Witness 構築（ボトムアップ）

新しい貢献は、導出履歴から witness $\sigma$ を抽出することである。アルゴリズムは後方（最終状態から初期状態へ）に witness を構築する。

1. 基底ケース: 最終節集合 $N_m$ に $X$ が含まれていない場合、恒等置換が witness となる。
2. 帰納ステップ: $N_{i-1}$ を $N_i$ に変換する各導出ステップ $S_i$ について、$\sigma_i$ が $N_i$ の witness であるならば、$\tau_{S_i}\sigma_i$ が $N_{i-1}$ の witness となるような置換 $\tau_{S_i}$ を計算する。
   • 標準的な推論ステップ（解決、因数分解など）の場合、$\tau$ は恒等である。
   • 拡張純粋性削除の場合、$\tau$ は極性に応じて $X$ を $\top$ または $\bot$ に設定する。
   • 精製節削除（複雑なケース）の場合、アルゴリズムは削除された節の局所解決閉包に基づいて witness を構築する。

C. 無限 Witness の処理

精製節に使用される解決閉包は無限になり得るため、無限の witness（無限論理積として表現される）が生じる可能性がある。本論文は 2 つの解決策を導入する。

1. 不動点 Witness: 無限の witness を、不動点論理における**最大不動点（gfp）**として表現する。これにより、潜在的に無限の定義の有限な表現が得られる。
2. 第一階 Witness（非循環条件）: 著者らは$k$-非循環精製と呼ばれる条件を定義する。削除ステップに関連する「精製包含グラフ」が非循環である場合、解決閉包の有界な反復を用いて、有限の第一階述語として witness を計算できる。

3. 主要な貢献

1. WSCAN アルゴリズム: 節集合に対する SOQE の witness を計算する完全な手法であり、SCAN アルゴリズムを拡張したもの。
2. 正しさの証明:
   • 構築された置換 $\sigma$ が有効な witness であること（$\exists X N \equiv N\sigma$）の証明。
   • witness 構築の論理から導出された、元の SCAN アルゴリズムに対する新しい正しさの証明。
3. 第一階 Witness の保証: 結果としての witness が第一階論理式となる（無限または不動点表現を避ける）ことを保証する非循環精製条件の特定。
4. Ackermann の補題の拡張: 著者らは、自らの手法が Ackermann の補題（SOQE の古典的手法）を包含し、述語が混合極性で現れる場合に拡張することを証明する。
5. 背景理論の処理: 等式推論（パラモジュレーション経由）および第一階背景理論の処理に手法を拡張し、グラフ到達可能性問題や他の制約付き Horn 節問題の解決を可能にする。
6. プロトタイプ実装: GAPT（General Architecture for Proof Theory）ソフトウェアパッケージ（バージョン 2.19.0）におけるプロトタイプ実装。

4. 結果と評価

• 実装: プロトタイプは 44 の例（文献および独自のもの）でテストされた。
• パフォーマンス:
  • 10 秒のタイムアウト内で、90.9% の例（40/44）に対して SCAN 導出が見つかった。
  • witness 計算は導出の発見（平均 375 ms）と比較して極めて高速で、平均0.619 msであった。
  • witness のサイズは一般的に小さかった（平均 6.9 記号）。
• 能力: 以前は無限の witness を生じたり、不動点論理を必要としたりした導出に対して、特に非循環精製グラフを伴うケースにおいて、システムは成功裡に第一階 witness を計算した。
• 限界:
  • 本手法は入力が節集合（全称量化されたドメイン変数）であることを必要とする。
  • Skolem 化が必要であり、かつ逆転不可能なケース（例：$\exists X \exists u \exists v (X(u) \land \neg X(v))$）は処理できない。なぜなら、結果としての witness には元の言語に存在しない Skolem 定数が含まれるためである。
  • 導出の探索空間は大きくなり得る。現在の実装はバックトラッキングを使用するが、大規模な節集合に対しては最適化されていない。

5. 意義

この研究は、単に量化子を除去するツールであった SCAN アルゴリズムを、除去された述語の定義を合成するツールへと変容させた点で重要である。

• 理論的架け橋: 第二階量化子除去（SOQE）と論理式方程式（FEQ）の分野を統合し、これらが同じコインの裏表であることを示す。
• 実用的応用: 明示的な第一階定義（witness）を提供することにより、本手法は以下の分野に直接適用可能である。
  • 知識表現: 論理的構造を保持しつつ、述語を忘却し、一様補間子を作成する。
  • 検証: プログラム検証のためのループ不変式を自動的に生成する（制約付き Horn 節を解く）。
  • モダリティ論理: モダリティ論理の対応公理を計算する。

本論文は、広範なクラスの導出（非循環精製グラフを有するもの）に対して、複雑な第二階の問題が、有限の第一階 witness を見つけることに帰着され得ることを確立し、自動推論のための強力な新しいツールを提供する。