Machine-Checked Formalization of Earlier Arguments on versus Using Isabelle/HOL
arXiv:cs/0310060
summary
The paper revisits an earlier argument about P versus NP based on the Subset‑Sum problem and provides a machine‑checked formalization of that argument in Isabelle/HOL, clarifying its logical structure by separating the combinatorial core from the universality principle for deterministic algorithms.
Abstract
This letter revisits an earlier argument concerning versus 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.
3 pages
Topics & keywords
#p vs np#subset sum#formal verification#isabelle/holl#complexity theoryP vs NPSubset‑SumIsabelle/HOLformalizationdeterministic algorithms