命题证明系统

在命题微积分和证明复杂性中，命题证明系统（pps），也称为Cook-Reckhow命题证明系统，是一个用于证明经典命题同义词的系统。

形式上，一个pps是一个多项式时间函数P，其范围是所有命题同义词的集合（表示TAUT）。如果A是一个公式，那么任何一个x使P(x)=A，就被称为A的P证明。定义pps的条件可以分解如下。

完整性：每个命题同义词都有一个P-证明，健全性：如果一个命题公式有一个P-证明，那么它就是一个同义词，效率。

一般来说，一个语言L的证明系统是一个范围为L的多项式时间函数，因此，一个命题证明系统是TAUT的证明系统。有时，人们会考虑以下的替代定义：一个pps被给定为一个有两个输入的证明-验证算法P(A,x)。

如果P接受一对(A,x)，我们就说x是A的一个P证明。P被要求在多项式时间内运行，此外，当且仅当A是一个同义词时，它必须持有A的一个P证明。

如果根据第 一个定义，P1是一个PPS，那么根据第二个定义，当且仅当P1(x)=A时，由P2(A,x)定义的P2是一个PPS。反过来说，如果根据第二个定义，P2是一个pps，那么P1的定义为

人们可以把第二个定义看作是解决TAUT中成员资格的非决定性算法。这意味着，证明pps的超多项式证明大小下限将排除基于该pps的某类多项式时间算法的存在。

作为一个例子，鸽子洞原理的解析中的指数级证明大小下限意味着任何基于解析的算法都不能有效地决定TAUT或SAT，并且在鸽子洞原理的同义词上会失败。这一点很重要，因为基于解析的一类算法包括目前大多数的命题证明搜索算法和现代工业SAT求解器。

在历史上，弗雷格的命题微积分是xxx个命题证明系统。命题证明系统的一般定义是由StephenCook和RobertA.Reckhow（1979）提出的。

命题证明系统可以用p-simulation的概念来比较。当存在一个多项式时间函数F，使P(F(x))=Q(x)对每一个x而言，一个命题证明系统P模仿Q(写成P≤pQ)，也就是说，给定一个Q证明x，我们可以在多项式时间内找到相同同义词的P证明。如果P≤pQ，Q≤pP，则证明系统P和Q是p等价的。

还有一个更弱的模拟概念：如果存在一个多项式p，使得对于同义词A的每一个Q-证明x，都有一个A的P-证明y，使得y的长度|y|最多为p(|x|)，则一个ppsP模拟或弱p-模拟一个ppsQ。(有些作者将p-模拟和仿真这两个词交替用于这两个概念中的任何一个，通常是指后者)。

如果一个命题证明系统能p模拟所有其他的命题证明系统，那么它就被称为p最优，如果它能模拟所有其他的pps，那么它就是最优的。

如果每个同义词都有一个短的（即多项式大小的）P-证明，那么一个命题证明系统P就是多项式约束的（也称为超）。如果P是多项式有界的，Q模拟P，那么Q也是多项式有界的。命题同义词的集合，TAUT，是一个coNP-complete集合。

一个命题证明系统是TAUT中成员资格的证明者。一个多项式有界的命题证明系统的存在意味着存在一个具有多项式大小证书的验证者，即TAUT在NP中。事实上这两个说法是等价的，即当且仅当复杂度类NP和coNP相等时，存在一个多项式约束的命题证明系统。

模拟或p-模拟下的证明系统的一些等价类与有界算术的理论密切相关；它们本质上是有界算术的非统一版本，就像电路类是基于资源的复杂性类的非统一版本一样。

例如，扩展的弗雷格系统（根据定义允许引入新的变量）以这种方式对应于多义性有界系统。