A Strategy Language for Controlled Proof Search

技術要約：制御された証明探索のための戦略言語

問題提起
自動推論において、論理体系の静的な完全性（任意の定理に対して証明が存在すること）は、プローバの動的な完全性（実際にその証明を見つけ出す能力）を保証するものではない。半決定可能な論理においては、推論規則が無限の成功者（successor）を生成する場合がある。もし証明探索戦略が不公平な探索（例えば、ある分岐を無期限に優先してしまうナイーブな深さ優先探索など）を採用した場合、関連する推論を永遠に後回しにし、有効な証明が存在する場合でも発見に失敗する可能性がある。この問題は、推論規則と証明探索戦略を分離しているPgeonのようなフレームワークにおいて特に深刻であり、探索ポリシーの設計が成功の決定的な要因となる。

手法
本論文では、論理体系の宣言的仕様を実行可能なプローバへとコンパイルするメタプローバ・フレームワークであるPgeonのための、形式的な戦略言語を導入する。核心となる手法論的転換は、証明探索を状態間の関係としてではなく、ストリームによる証明状態の列挙としてモデル化することにある。

1. 形式意味論： 証明状態（$\Sigma$）は、部分的に構築された証明木の集合として扱われる。戦略は、状態をストリーム（有限または無限の成功者の集合）へと写像する関数 $s: \Sigma \to \text{Str}(\Sigma)$ として定義される。これにより、非決定性が明示的に扱われる：

   • 空のストリームは失敗を表す。
   • 単一要素のストリームは決定的な成功を表す。
   • 複数の要素を持つストリームは非決定的な分岐を表す。
   • 無限ストリームは、無制限に多くの成功者を生成できる規則を表す。

2. コンビネータ： この言語は、これらの戦略を合成するためのオペレータ群を提供し、偏った（深さ優先）探索と公平な（インターリーブによる）探索を区別する：

   • 順次合成 ($;$)： ある戦略の結果に対して別の戦略を適用する。
   • 左偏重選択 ($\parallel$)： 最初の戦略を試行し、それが失敗（空のストリーム）した場合に、第2の戦略へフォールバックする。
   • 公平な順次合成 ($\&;$)： 対角線論法（$\triangle$）を用いて順次適用の結果をインターリーブし、もし結果が有限ステップで到達可能であれば、それが最終的に探索されることを保証する。
   • 公平な選択 ($\&|$)： 2つの代替戦略の結果を公平にインターリーブする。
   • 反復 ($*$)： 公平な順次合成（$\mu X. \text{id} \&; (s \&; X)$）を用いた最小不動点として定義され、すべての有限の反復深度が探索されることを保証する（厳密な深さ優先には進まない）。

3. プリミティブ操作： 言語には、プリミティブな規則（$r$）と、状態内のすべての許容されるマッチングに規則を適用する全適用オペレータ（$r!$）が含まれる。

主要な貢献

• 合成的なストリーム意味論： 本論文は、探索空間が第一級オブジェクト（ストリーム）として再構成される、戦略コンビネータの合成的な代数を提供している。これにより、スタック規律や継続といった実装の詳細とは独立して、公平性と列挙について推論することが可能になる。
• 公平性のメカニズム： 対角線論法に基づくインターリーブ演算子（$\&;$ および $\&|$）を導入することで、無限の分岐が有限の証明の発見を妨げる「飢餓（starvation）」の問題に対処している。
• Pgeonのための形式的戦略言語： 本研究は、Pgeonフレームワークの戦略コンポーネントを形式化し、証明探索の制御フローを宣言的な言語へと抽象化している。

結果およびケーススタディ
著者らは、以下の2つのケーススタディを通じて、提案手法の表現力と有効性を実証している。

1. 一階述語論理 (LK)： 著者らは、閉包（単一化）と規則の飽和の相互作用に対処している。単純な繰り返し規則適用の戦略は、特定のインスタンス化に早くコミットしすぎるため、しばしば証明を見つけることに失敗する。提案された戦略 $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$ は、公平な合成を用いて、閉包の試行と規則の飽和をインターリーブする。これにより、異なる単一化の選択肢がすべての探索深度にわたって探索されることが保証され、閉じる導出を見逃しながら無限のインスタンス化ループに陥ることを防ぐ。

2. 様相論理 (S4)： S4においては、S4の様相規則の適用を可能にするために、数式の任意の除去を行う非決定的な規則 $\theta$ が必要であるが、これは閉包に必要な数式を破棄してしまうリスクを伴う。制御されていない $\theta$ の使用はデッドエンドを招く。著者らは、S4の適用を可能にするための数式の除去方法を公平に探索する、組み合わせ戦略 $\theta^* \&; \text{S4}$ を提案している。これは、より大きな戦略 $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$ に統合されており、もしS4の成功的な適用に特定の数式の集合の除去が必要な場合でも、その構成が飢餓なしに最終的に到達できることを保証している。

意義
本論文は、このアプローチが、証明探索手順を指定し分析するための、原理に基づいたモジュール式の基礎を提供すると主張している。推論規則と探索戦略を分離し、合成的な意味論を持つ形式的な言語を提供することで、本フレームワークは、半決定可能な論理における探索空間の系統的な探索を可能にする。これは、ナイーブな深さ優先戦略が失敗する場合でも、ストリームのインターリーブを通じて公平性を明示的に管理することで、動的な完全性を達成できることを示している。本研究は、プローバの具体的な実装とは独立して、抽象的なレベルで証明探索の手順について推論することを可能にするものである。