命題証明システム

命題計算と証明の複雑性において、命題証明システム( pps )は、クック・レックハウ命題証明システムとも呼ばれ、古典的な命題トートロジーを証明するシステムです。

数学的な定義

正式には、ppsは多項式時間関数Pであり、その値域はすべての命題トートロジーの集合（TAUTと表記）である。^[1]Aが式である場合、 P ( x ) = Aとなる任意のxはAのP証明と呼ばれる。ppsを定義する条件は次のように分解できる。

完全性: すべての命題トートロジーはP証明を持つ。
健全性: 命題論理式がP証明を持つ場合、それはトートロジーである。
効率: P は多項式時間で実行されます。

一般に、言語Lの証明システムは、値域がLである多項式時間関数です。したがって、命題証明システムは TAUT の証明システムです。

次のような代替定義が考慮されることもあります。pps は、2 つの入力を持つ証明検証アルゴリズムP ( A、x ) として与えられます。Pがペア ( A、x ) を受け入れる場合、 x はAのP証明であると言います。Pは多項式時間で実行される必要があり、さらに、 AがP証明を持つのは、それがトートロジーである場合のみである必要があります。

P ₁が最初の定義によるppsである場合、 P _{2 は}P ₂ ( A , x )によって定義され、P ₁ ( x ) = Aが2番目の定義によるppsである場合に限ります。逆に、P ₂が2番目の定義によるppsである場合、P _{1 は}次のように定義されます。

P_{1}(\langle x,A\rangle)={\begin{cases}A&{\text{if }}P_{2}(A,x)\\\top &{\text{otherwise}}\end{cases}}

( P _{1 は}ペアを入力として受け取ります) は最初の定義によれば pps であり、は固定されたトートロジーです。 $\top$

アルゴリズム解釈

2 番目の定義は、TAUT のメンバーシップを解決するための非決定論的アルゴリズムとして見ることができます。これは、pps の超多項式証明サイズの下限を証明すると、その pps に基づく特定のクラスの多項式時間アルゴリズムの存在が排除されることを意味します。

たとえば、鳩の巣原理の解決における指数的な証明サイズの下限は、解決に基づくアルゴリズムは TAUT または SAT を効率的に決定できず、鳩の巣原理のトートロジーで失敗することを意味します。解決に基づくアルゴリズムのクラスには、現在の命題証明検索アルゴリズムと現代の産業用 SAT ソルバーのほとんどが含まれるため、これは重要です。

歴史

歴史的には、フレーゲの命題計算が最初の命題証明システムでした。命題証明システムの一般的な定義は、スティーブン・クックとロバート・A・レックハウ（1979）によるものです。^[1]

計算複雑性理論との関係

命題証明システムは、p-シミュレーションの概念を使って比較することができます。命題証明システムPは、あらゆる xに対してP ( F ( x )) = Q ( x )となる多項式時間関数Fが存在するとき、 Q ( P ≤ _p Qと表記) を p-シミュレートします。^[1]つまり、Q証明xが与えられれば、同じトートロジーのP証明を多項式時間で見つけることができます。 P ≤ _p QかつQ ≤ _p Pの場合、証明システムPとQはp-同等です。より弱いシミュレーションの概念もあります。トートロジーAのあらゆる Q 証明 x に対して、 y の長さ、| y | が最大で p (| x |) となるようなAのP証明yが存在するような多項式pが存在するとき、pps Pはpps Qをシミュレート、または弱くp-シミュレートします。 (著者の中には、p-シミュレーションとシミュレーションという単語を、これら 2 つの概念のいずれか (通常は後者) に対して互換的に使用する人もいます。)

命題証明システムは、他のすべての命題証明システムをpシミュレートする場合にp 最適と呼ばれ、他のすべての pp をシミュレートする場合は最適です。すべてのトートロジーに短い (つまり、多項式サイズの) P証明がある場合、命題証明システムPは多項式的に有界です(スーパーとも呼ばれます) 。

Pが多項式的に制限され、Q がP をシミュレートする場合、Qも多項式的に制限されます。

命題トートロジーの集合 TAUT はcoNP完全集合である。命題証明システムは、TAUT のメンバーシップの証明書検証器である。多項式的に制限された命題証明システムの存在は、多項式サイズの証明書を持つ検証器が存在すること、つまり TAUT がNPに含まれることを意味する。実際、これら 2 つのステートメントは同等であり、つまり、複雑性クラス NP とcoNPが等しい場合にのみ、多項式的に制限された命題証明システムが存在する。^[1]

シミュレーションまたはpシミュレーションによる証明システムの同値クラスの一部は、有界算術の理論と密接に関連しています。これらは本質的に有界算術の「非一様」バージョンであり、回路クラスがリソースベースの複雑性クラスの非一様バージョンであるのと同じです。「拡張フレーゲ」システム (定義により新しい変数の導入が可能) は、このようにして、たとえば多項式有界システムに対応します。有界算術が回路ベースの複雑性クラスに対応する場合、証明システムの理論と回路ファミリの理論には、下限結果と分離の一致など、類似点がよくあります。たとえば、指数以下のサイズの回路ファミリではカウントを実行できないのと同様に、鳩の巣原理に関連する多くのトートロジーは、深さが制限された式に基づく証明システムでは指数以下の証明を持つことができません (特に、解像度ベースのシステムでは深さ 1 の式のみに依存するため、この証明システムでは指数以下の証明を持つことができません)。 $\mathbf {AC} ^{0}$