2026-07-23T17:34:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13915 2024-03-06T10:53:07Z ddc:004 open_access

Mechanising Complexity Theory: The Cook-Levin Theorem in Coq Gäher, Lennard Kunze, Fabian computational model NP completeness Coq Cook Levin We mechanise the Cook-Levin theorem, i.e. the NP-completeness of SAT, in the proof assistant Coq. We use the call-by-value λ-calculus L as the model of computation to formalise time complexity, the class NP, and polynomial-time reductions. The latter two notions agree with the usual characterisations via Turing machines (TMs), as L and TMs are polynomial-time equivalent. The use of L as the computational model, as opposed to TMs, significantly eases program verification and the derivation of resource bounds. However, for showing the NP-hardness of SAT, computations of L need to be encoded in SAT, which is complicated by L’s more complex computational structure. Thus, the polynomial-time reduction chain to SAT employs TMs as an intermediate problem, for which we neatly factor out a known textbook reduction from TMs to SAT. Still, all reduction functions are implemented and analysed in L. To the best of our knowledge, this is the first result in computational complexity theory that has been mechanised with respect to any concrete computational model. We discuss what makes this area of computer science hard to mechanise and highlight the design choices which enable our mechanisations. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lennard Gäher and Fabian Kunze 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.20 urn:nbn:de:0030-drops-139154 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.20 eng https://creativecommons.org/licenses/by/4.0/legalcode