Machine-Checked Formalization of Earlier Arguments on ℙ versus \mathbbNP Using Isabelle/HOL

2003/10/31 by Craig Alan Feinstein, Feinstein, Craig Alan · 1 voice
Computer Science · Engineering · #Cellular Automata and Applications #Computability, Logic, AI Algorithms #Computational Complexity (cs.CC) #FOS: Computer and information sciences #cs.CC #graph theory and CDMA systems

paper · pdf · doi:10.48550/arxiv.cs/0310060

openalex publication_date 2003/10/31 · arxiv published 2003/10/31 · openalex created_date 2025/10/10 · arxiv updated 2026/07/13 · openalex updated_date 2026/07/28

Abstract

This letter revisits an earlier argument concerning ℙ versus \mathbbNP based on the SUBSET-SUM problem and examines its formalization in Isabelle/HOL. The formal development clarifies the argument's logical structure by separating its deductive combinatorial core from the broader universality principle required to extend it to all exact deterministic algorithms.

Discussions

• I wrote that paper. Over the last two years I have been working on formalizing similar arguments about P versus NP in the Isabelle/HOL proof assistant. In doing so, I discovered exactly where the diff [stackexchange, 3 points]

Related

• Inconsistency of the Zermelo-Fraenkel set theory with the axiom of choice and its effects on the computational complexity
• Polynomial time logic: Inability to express
• Simple proof of Zermelo's theorem
• Lifting up the proof theory to the countables : Zermelo-Fraenkel set theory
• An arguable inconsistency in ZF