A Mechanical Proof of the Cook-Levin Theorem
A Mechanical Proof of the Cook-Levin Theorem
复制标题
库克-莱文定理的机械证明
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
J. Cowles
中科院分区：
文献类型：
--
作者：
Ruben Gamboa;J. Cowles
与复杂性理论中的许多定理一样，著名的库克-莱文定理的典型证明（显示可满足性的 NP 完备性）是基于巧妙的构造。库克-莱文定理是通过仔细地将图灵机的可能计算转换为布尔表达式来证明的。当布尔表达式被构建时，很明显，当且仅当计算对应于图灵机的有效且可接受的计算时，它才能被满足。关于翻译作品如宣传的那样的争论细节通常被掩盖；讨论的是翻译本身。在本文中，我们提出了翻译正确性的正式证明。该证明通过定理证明器 ACL2 进行了验证。
As is the case with many theorems in complexity theory, typical proofs of the celebrated Cook-Levin theorem showing the NP-completeness of satisfiability are based on a clever construction. The Cook-Levin theorem is proved by carefully translating a possible computation of a Turing machine into a boolean expression. As the boolean expression is built, it is obvious that it can be satisfied if and only if the computation corresponds to a valid and accepting computation of the Turing machine. The details of the argument that the translation works as advertised are usually glossed over; it is the translation itself that is discussed. In this paper, we present a formal proof of the correctness of the translation. The proof is verified with the theorem prover ACL2.