A mechanical proof of the Cook-Levin theorem

DOI10.1007/978-3-540-30142-4_8MaRDI QIDQ5464665zbMATH OpenOpenAlexFDO

Authors Ruben A. Gamboa, John Cowles

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Church meets Cook and Levin
• Proof pearl: proving a simple von Neumann machine Turing complete
• The complexity of satisfiability problems
• Proving completeness by logic
• scientific article; zbMATH DE number 1179974

Cited in

(4)

• Proof pearl: proving a simple von Neumann machine Turing complete
• Church meets Cook and Levin
• The Cook-Levin theorem
• A mechanized proof of the basic perturbation lemma

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: A mechanical proof of the Cook-Levin theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5464665)