命题演算系统

从形式上看，pps是一个多项式时间函数P，其中P 的值域是所有命题重言式的集合（用TAUT来表示）。如果A是一个公式，那么任何使得P（x）= A 成立的 x 称作 A 的P-证明。定义pps的条件可以分解如下:

• 完整性：每个命题重言式有一个P-证明，
• 可靠性：如果命题公式具有P-证明，那么这个命题为重言式，
• 效率性：P 可在多项式时间内运算。

一般来说，一种语言 L 的证明系统是一个多项式时间函数，其值域是L。因此，命题证明系统是TAUT的证明系统。

有时会考虑使用如下的第二定义：给出具有两个输入验证算法P（A,x）作为pps。 如果 P 接受一个数据对（A, x），我们称x 是A 的一个P-证明。 P 需要在多项式时间内运算，而且，它必须始终满足当且仅当A 是重言式时才存在P-证明。

如果P₁是根据第一个定义产生的pps，当且仅当P₁（x）= A 时，由P₂（A,x ) 定义的P₂ 是一个pps。反之，如果P₂是根据第二个定义产生的pps，如下定义的P₁

（P₁ 将一对数据作为输入）是根据第一个定义的pps，其中   是固定的重言式。

人们可以把第二个定义看作是一个非确定性的算法，用于求解TAUT中的隶属关系。这意味着证明pps的超多项式的证明大小下界将不可能存在基于该pps的某类多项式时间算法。

例如， 抽屉原理在归结原理中的指数证明大小下界意味着任何基于归结原理的算法都不能有效地判断TAUT或SAT，并将在抽屉原理重言式中失效。这很重要，因为基于归结原理的一类算法包括大多数目前的命题证明搜索算法和现代SAT求解算法。

历史上， 弗雷格命题演算是第一个命题证明系统。命题证明系统的一般定义是由斯蒂芬·库克和罗伯特·雷克霍（1979）确立的。^[1]

命题证明系统可以与p-模拟的概念比较。当存在多项式时间函数 F 使得对任意的x 有P（F（x））= Q（x）时，称命题证明系统 P p-模拟 Q （写作P ≤_pQ）。^[1]也就是说，给定一个Q-证明 x，我们可以在多项式时间内找到对于相同重言式的P-证明。如果 P ≤_pQ 且 Q ≤_pP，证明系统 P 和 Q 是 p-等价的。还有一个更弱的p-模拟的概念：pps P 模拟 或者 弱p-模拟 pps Q 如果存在多项式 p 使得对于每个重言式A的Q-证明 x，存在一个A 的P-证明 y 使得y 和|y |的范围最多是p(|x|)。(有些作者对这两个概念混用p-模拟和模拟两个词，通常使用后者。)

如果命题证明系统p-模拟所有其他命题证明系统，该系统被称为p-最优的，如果它模拟所有其他pps，它自然也是最优的 。如果每个重言式都有一个短小的（即多项式大小）P-证明，则命题证明系统P 是多项式有界的 (也称为super)。

如果P 多项式有界且 Q 模拟 P，那么Q 也是多项式有界的。

命题重言式的集合TAUT是一个coNP完全问题集合。命题证明系统是TAUT隶属关系的证书验证器。多项式有界命题证明系统的存在意味着存在一个具有多项式大小证书的验证器，即NP中的TAUT。事实上，这两个陈述是等价的，即当且仅当复杂性NP和coNP等价时，^[1]才存在一个多项式有界的命题证明系统。

一些模拟或p-模拟下的等价类证明系统与有界算术理论密切相关；它们本质上是有界算术的“非统一”版本，就像电路类是基于资源的复杂性类的非统一版本一样。例如，“扩展弗雷格”系统（允许通过定义引入新变量）以这种方式对应于多项式有界系统。当有界算术反过来对应于基于电路的复杂性类时，证明系统理论和电路族理论之间通常有相似之处，如匹配下界结果和分离。例如，正如计数不能由次指数大小的   电路族完成，许多与抽屉原理相关的重言式在基于有限深度公式的证明系统中没有次指数证明（特别是在基于分辨率的系统中，因为它们仅依赖于深度为1的公式）。

经研究的命题证明系统的一些例子有：

• 命题归结原理以及它的各种限制和扩展，如DPLL算法
• 自然演绎
• 相继式演算
• 弗雷格系统
• 扩展弗雷格系统
• 多项式演算
• 零点系统
• 切割平面法