How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Vertex cover polynomial-time many-one reduces to set cover
Statement
VERTEX COVER polynomial-time many-one reduces to SET COVER.
Facts & Assumptions
Given: A VERTEX COVER instance , where .
A polynomial-time many-one reduction is a total polynomial-time function preserving membership in both directions, by Polynomial-time many-one reductions.
A vertex cover is a subset of vertices meeting every edge, by Clique, independent set, and vertex cover decision problems.
A set cover chooses at most members of a family of subsets whose union is the whole universe, by The set cover decision problem.
Proof
Let the SET COVER universe be the edge set . For each vertex , define the subset . Output the SET COVER instance . This is computable in polynomial time by scanning the incidence relation of .
If is a vertex cover with , then every edge of has an endpoint in . Equivalently, every element of lies in one of the sets with . Hence is a set cover of size at most .
Conversely, if is a set cover of size at most , then every edge belongs to some with . By definition of , that means is an endpoint of . Therefore is a vertex cover of size at most .
Steps 2.1 and 2.2 prove . By [L1], the construction in step 1.1 is a polynomial-time many-one reduction.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Fabrizio Iozzi and Luca Trevisan, Handout NP3 (standard reference, not scraped)