As is the case with many theorems in complexity theory, typical proofs of the celebrated Cook-Levin theorem showing the NPcompleteness 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. © Springer-Verlag 2004.
CITATION STYLE
Gamboa, R., & Cowles, J. (2004). A Mechanical Proof of the Cook-Levin Theorem. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3223, 99–116. https://doi.org/10.1007/978-3-540-30142-4_8
Mendeley helps you to discover research relevant for your work.