逻辑与计算复杂性的交汇
斯蒂芬·库克（Stephen A. Cook）是以计算复杂性和数理逻辑研究著称的计算机科学家。他于1961年毕业于密歇根大学，1966年取得哈佛大学博士学位；随后任职于加州大学伯克利分校，1970年加入多伦多大学，1982年获得图灵奖。
库克研究的不是某一台计算机能运行多快，而是计算问题在资源限制下的共同结构。其学术范围还涉及程序语言语义、并行计算及逻辑与复杂性之间的联系。1971年的命题定理证明复杂度论文，是这一研究方向中的关键成果，而不是其全部工作。
参考：[1]
把计算历史写成逻辑公式
《定理证明过程的复杂性》的核心构造，是把一台多项式时间非确定型图灵机的接受计算转写为命题公式。变量分别描述每个时刻的带符号、机器状态和读写头位置；一组约束要求初始配置正确、每一步转移合法，并最终到达接受状态。
由于计算步数有多项式上界，所需描述也能在多项式时间内构造。所得合取范式公式可满足，当且仅当原机器存在接受该输入的计算过程。证明因此把“存在一条可行计算路径”转换成“存在一组满足公式的真假赋值”，建立了不同问题之间可复用的连接。
原论文与后来的统一表述
原论文正式使用带查询机的多项式时间归约，并把重言式判定放在显著位置；重言式要求所有赋值都使公式为真，可满足性只要求存在一种赋值，二者不能直接混称。不过，论文构造已经给出了后来SAT的NP完全性表述所需的关键内容。
卡普在1972年进一步用多项式时间多对一归约连接一批组合问题。列昂尼德·列文则独立研究通用搜索问题，其1973年论文包含可满足性等例子。后来的“库克—列文定理”名称汇合了独立研究传统，并不是两人共同署名发表了库克的1971年论文。
完全性不是难解性的最终证明
P关注能够在多项式时间内求解的判定问题；NP关注肯定答案具有可在多项式时间内核验的证书的问题。NP完全性要求问题自身属于NP，并且所有NP问题都能归约到它。因此，如果某个NP完全问题获得多项式时间算法，就会得到P等于NP。
这项结论没有证明P不等于NP，Clay数学研究所仍将该问题列为未解难题。也不能从NP完全性推出每个具体实例都难，更不能把实用SAT求解器的快速表现当作一般复杂性问题已经解决。库克建立的是研究难度关系的理论基础，后续求解算法和工程系统还有各自的作者、方法及适用范围。