命題計算およびにおいて、命題証明系（めいだいしょうめいけい、、ppsとも呼ばれ、クック＝レックホウ命題証明系とも呼ばれる）とは、古典命題トートロジーを証明するための体系である。
数学的定義 形式的には、ppsとは、その値域がすべての命題トートロジーの集合（TAUTと表記される）である多項式時間関数 P のことである。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-証明を持つことと、それがトートロジーであることとが同値でなければならない。
P1 が最初の定義によるppsであるならば、P2(A,x) が P1(x) = A であることと同値であるように定義された P2 は、第二の定義によるppsである。逆に、P2 が第二の定義によるppsであるならば、
によって定義される（対を入力として取る）P1 は、最初の定義によるppsである。ここで は固定されたトートロジーである。
アルゴリズム的解釈 第二の定義は、TAUTへの帰属を解くための非決定性アルゴリズムとみなすことができる。これは、あるppsについての超多項式的な証明サイズの下界を証明することが、そのppsに基づく特定のクラスの多項式時間アルゴリズムの存在を排除することを意味する。
例として、鳩の巣原理についての導出原理における指数関数的な証明サイズの下界は、導出原理に基づくいかなるアルゴリズムもTAUTあるいはSATを効率的に決定することはできず、鳩の巣原理のトートロジーにおいて失敗することを含意する。これは、導出原理に基づくアルゴリズムのクラスが、現在のほとんどの命題証明探索アルゴリズムや現代の産業用SATソルバーを含んでいるため、重要である。
歴史 歴史的には、フレーゲの命題計算が最初の命題証明系であった。命題証明系の一般的な定義は、スティーヴン・クックとロバート・A・レックホウ（1979年）によるものである。
計算複雑性理論との関係 命題証明系は、の概念を用いて比較することができる。命題証明系 P が Q を「p-シミュレートする」（P ≤pQ と書かれる）とは、すべての x について P(F(x)) = Q(x) であるような多項式時間関数 F が存在することをいう。すなわち、Q-証明 x が与えられたとき、同じトートロジーの P-証明を多項式時間で見つけることができる。P ≤pQ かつ Q ≤pP であるならば、証明系 P と Q は「p-同値」である。シミュレーションにはより弱い概念もある。あるpps P が、あるpps Q を「シミュレートする」あるいは「弱くp-シミュレートする」とは、あるトートロジー A のあらゆる Q-証明 x について、その長さ |y| が p(|x|) 以下であるような A の P-証明 y が存在するような多項式 p が存在することをいう。（一部の著者は、これら2つの概念のいずれについても、通常は後者について、p-シミュレーションとシミュレーションという語を互換的に用いる。）
命題証明系は、それが他のすべての命題証明系をp-シミュレートするとき「p-最適」と呼ばれ、他のすべてのppsをシミュレートするとき「最適」であるという。命題証明系 P は、すべてのトートロジーが短い（すなわち多項式サイズの）P-証明を持つとき、「多項式的に有界」（「super」とも呼ばれる）である。
P が多項式的に有界であり、Q が P をシミュレートするならば、Q もまた多項式的に有界である。
命題トートロジーの集合TAUTは、Co-NP完全な集合である。命題証明系は、TAUTへの帰属のための証明書検証者である。多項式的に有界な命題証明系の存在は、多項式サイズの証明書を持つ検証者が存在すること、すなわちTAUTがNPに属することを意味する。実際、これら2つの言明は同値である。すなわち、多項式的に有界な命題証明系が存在することと、計算複雑性クラスNPとCo-NPが等しいこととは同値である。
シミュレーションあるいはp-シミュレーションのもとでの証明系のいくつかの同値類は、の理論と密接に関連している。それらは本質的に有界算術の「非一様」版であり、これは回路計算量クラスが資源に基づく計算複雑性クラスの非一様版であるのと同様である。例えば、（定義による新しい変数の導入を許す）「拡張フレーゲ」系は、この意味で多項式的に有界な体系に対応する。有界算術が回路に基づく計算複雑性クラスに対応するところでは、証明系の理論と回路族の理論との間に、下界の結果や分離の一致といった類似性がしばしば見られる。例えば、計数が劣指数サイズの回路族によっては行えないのとちょうど同じように、鳩の巣原理に関連する多くのトートロジーは、有界深さの論理式に基づく証明系においては劣指数証明を持つことができない（特に、導出に基づく体系では、それらは深さ1の論理式のみに依拠するため、持つことができない）。
命題証明系の例
研究されている命題証明系の例としては、以下のものがある。 命題導出原理、およびDPLLアルゴリズムのようなその様々な制限や拡張 自然演繹 シークエント計算 フレーゲ系
切除平面法 タブローの方法
出典
さらなる読書 Samuel Buss (1998), "An introduction to proof theory", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier (1998). P. Pudlák (1998), "The lengths of proofs", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier, (1998). P. Beame and T. Pitassi (1998). Propositional proof complexity: past, present and future. Technical Report TR98-067, Electronic Colloquium on Computational Complexity. Nathan Segerlind (2007) "The Complexity of Propositional Proofs", Bulletin of Symbolic Logic 13(4): 417–481 J. Krajíček (1995), Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press. J. Krajíček, Proof complexity, in: Proc. 4th European Congress of Mathematics (ed. A. Laptev), EMS, Zurich, pp. 221–231, (2005). Alexander A. Razborov, Propositional proof complexity, in: Proc. 8th European Congress of Mathematics, EMS, Portorož, pp. 439–464, (2023). J. Krajíček, Propositional proof complexity I. and Proof complexity and arithmetic. Stephen Cook and Phuong Nguyen, Logical Foundations of Proof Complexity, Cambridge University Press, 2010 (draft from 2008) Robert Reckhow, On the Lengths of Proofs in the Propositional Calculus, PhD Thesis, 1975.
外部リンク Proof Complexity