Resolution-Proof Redundancy¶
A propositional resolution proof is redundant under a node-count measure when a valid proof from the fixed inputs derives the same or a subsuming root with fewer proof-DAG nodes.
Core Idea¶
Resolution-proof redundancy is a property of a propositional resolution proof graph. Under the node-count measure in Fontaine, Merz, and Woltzenlogel Paleo, a proof is redundant when there is another valid resolution proof with a root clause equal to or subsuming the original root and strictly fewer total proof-DAG nodes.[1] This entry compares proofs using the same input clauses. That fixed-input restriction follows the paper's proof-from-a-clause-set setting and worked comparisons; it is an explicit curation limit rather than a separate phrase in its section 3 definition.[1]
Repeated clauses or pivots can point to possible savings, but they do not by themselves prove that a valid smaller alternative exists. The source's Example 6 shows a tempting global rewrite pattern whose specified replacements fail; that result does not prove the graph absolutely irreducible.[1]
Structural Signature¶
Four roles define the positive test:
- Original proof and fixed premises: a valid rooted resolution DAG from one clause set.
- Root-conclusion contract: an alternative must derive an equal or subsuming root clause.
- Valid alternative witness: every step in the smaller derivation must be a valid resolution inference.
- Strict node count: the alternative must contain fewer total DAG vertices, including input and inference nodes.
The paper defines resolution proofs as DAGs and measures their size by node count.[1] A shorter proof of an unrelated claim or a proposed rewrite with an invalid resolution step fails this entry's test.
Scope of Application¶
The method of comparison applies to propositional resolution proof DAGs. Fontaine and colleagues show a finite local refutation rewrite in Example 4 and an analytic eager-unit refutation family in Theorem 10.[1] Those are unlike configurations in one formal proof system, not a survey of all mathematical proofs or measured production SAT-solver logs.
Clarity¶
“Unnecessary step” can mean a repeated symbol, an applicable-looking rewrite rule, or an actual shorter valid derivation. The formal property requires the last. Example 6's three specified global replacements are invalid there, so that example is a narrow failure of those replacements and leaves the wider smaller-proof question open.[1]
Manages Complexity¶
The four-role test separates the proof object, the target conclusion, the alternative's validity, and the size comparison. That prevents a search heuristic or apparent duplicate from being mistaken for a proven reduction. It does not make finding a smaller proof easy; failure of one rewrite procedure is not a proof of minimality.[1]
Abstract Reasoning¶
Let P be the original proof and Q a proposed alternative from the same input clauses. Check that Q is valid, that its root equals or subsumes the root of P, and that its total node count is strictly lower. In the paper's Theorem 10 family at n = 3, the eager refutation has six resolution inferences plus four input nodes, whereas LowerUnits has three plus the same four: 10 versus 7 nodes.[1] That total-node comparison is derived from the source's inference counts and input set.[1]
Knowledge Transfer¶
The criterion holds across the local Example 4 and the distributed eager-unit family even though the repeated work looks different.[1] It should not be transferred unchanged to an informal proof or another formal calculus without defining its inference rules, fixed premises, conclusion relation, and size metric.
Examples¶
Local refutations. Example 4 shows two related original refutations, ψ1 and ψ2, that the authors rewrite to a shorter valid ψ3 refutation from the displayed premises.[1] They are variants of one local setting, not two independent applications.[1]
Mapped back: either original is the proof under test; its displayed clauses are the fixed premises; the empty root satisfies the conclusion contract; ψ3 is the valid alternative and has a lower node count.[1]
Eager-unit family. Theorem 10 compares eager-unit refutations of Sₙ with LowerUnits refutations.[1] It gives n(n+1)/2 versus n resolution inferences using the same n+1 input clauses; for n = 3, the total-node counts are 10 versus 7.[1] The example is a constructed family, not a measured solver run.[1]
Mapped back: the eager S₃ refutation is the proof under test; its four clauses are the fixed premises; both roots are empty; LowerUnits supplies a valid alternative with a strictly lower node count.[1]
Neighborhood in Abstraction Space¶
Resolution-Proof Redundancy sits in a moderately populated region (59th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Codes, Matrices & Combinatorial Problems (33 abstractions)
Nearest neighbors
- Resolution Proof Compression by Splitting — 0.88
- Intuitionistic Type Theory — 0.85
- GI (complexity) — 0.85
- GI-complete — 0.84
- Existential Quantification — 0.84
Computed from structural-signature embeddings · 2026-10-25
Not to Be Confused With¶
- Any repeated pivot: a clue for potential compression, not a positive witness.[1]
- Failure of one named rewrite: Example 6 does not establish absolute nonredundancy.[1]
- Resolution Proof Compression by Splitting: a specific algorithm; this entry is a property that any suitable shorter valid proof can witness.
- The catalog's Redundancy Prime: intentional duplicate components for fault tolerance, a different identity.
- A shorter proof from new premises: a changed comparison problem outside this entry's fixed-input rule.
References¶
[1] Fontaine, P.; Merz, S.; Woltzenlogel Paleo, B. “Compression of Propositional Resolution Proofs via Partial Regularization.” CADE (2011). Full original paper. Consulted §§2–4, especially proof DAG and node count (printed pp.238–239), Example 4 (pp.239–240), Example 6 (p.240), and Theorem 10 (p.243). The n = 3 total-node calculation adds the shared input nodes to the paper's inference counts. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s