P vs NP问题的提出缘起于“定理证明过程的复杂性（The Complexity of Theorem-Proving Procedures）”（1971年）。分享此文的部分译文。

定理证明过程的复杂性

摘要

文章指出，不确定性图灵机在多项式时间内解决的任何识别问题都可以“归约”为判定给定命题公式是否为重言式的问题。粗略说，这里“归约”意味着，如果第二个问题可用oracle解决，那么第一个问题就可以在多项式时间内确定性地解决。根据此归约的概念，定义了多项式复杂性，并且指出判定重言式的问题与判定两个给定图中的第一个图是否与第二个子图同构的问题具有相同的多项式复杂性。文章还讨论了其他例子，介绍和讨论了一种量度谓词演算证明过程复杂性的方法。

原文：https://www.inf.unibz.it/~calvanese/teaching/11-12-tc/material/cook-1971-NP-completeness-of-SAT.pdf

Cook定理译文.pdf