Skip to content

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.

Version
v1 · 2026-10-25 · History
Domain-specific #
14436
Domain group
Applied Sciences & Engineering
Origin domain
Computer Science & Software Engineering
Subdomains
Automated Reasoning, Proof Compression → Computer Science & Software Engineering
Aliases
Redundant resolution proof, Proof-DAG redundancy

Core Idea

Resolution-proof redundancy is a property of a propositional resolution proof graph under a specified size measure. For the node-count criterion used by Fontaine, Merz, and Woltzenlogel Paleo, a proof is redundant if another valid resolution proof derives the same or a subsuming root clause with strictly fewer nodes in its proof DAG.[1] This entry holds the input clauses fixed when comparing the proofs. That restriction follows the paper's proof-from-a-clause-set setting and its worked comparisons; section 3 does not restate it as a separate phrase in the definition.[1]

The property concerns an exhibited alternative derivation, not a visual impression that a pivot or clause has been used twice. In the paper's finite local example, a shorter refutation witnesses redundancy.[1] In a different analytic family, a LowerUnits refutation avoids repeated eager-unit work and uses fewer nodes.[1] Both derive the empty clause, but the second is a mathematical construction rather than an observed SAT-solver run.[1]

Structural Signature

Sig role-phrases:

  • Original proof and fixed premise set — supply a valid rooted resolution DAG and hold its input clauses constant for the comparison.
  • Root-conclusion contract — require the alternative root clause to equal or subsume the original root, so size is not improved by proving an unrelated claim.
  • Valid alternative witness — exhibit another correctly formed resolution DAG from those premises; a merely proposed invalid rewrite cannot witness the property.
  • Strict total-node comparison — count all vertices of each proof DAG, including input and inference nodes, and require the witness to be smaller.

These roles distinguish a formal property from a loose description of repeated work. A repeated pivot can suggest where compression might be found, but without a valid alternative, the property has not been established.[1] A smaller graph with a different premise set changes the comparison problem. A smaller derivation of an unrelated clause does not satisfy the root contract.[1]

What It Is Not

  • Not every duplicated phrase in a mathematical proof. The checked criterion belongs to propositional resolution proof DAGs and their node count; the source does not establish an all-proof-systems definition.[1]
  • Not merely a syntactic repeated-pivot pattern. A pattern can suggest a local or global rewrite, but validity and strict size reduction must still be shown.[1]
  • Not a claim that all failed rewrites prove irreducibility. The paper's Example 6 blocks the three specified replacements of Definition 5; it does not rule out every other smaller proof.[1]
  • Not a particular compression algorithm. Resolution Proof Compression by Splitting is a cataloged split-and-recombine procedure. The property here asks whether a valid shorter alternative exists, regardless of which algorithm finds it.
  • Not the catalog's fault-tolerance sense of Redundancy. That Prime concerns deliberate duplicate components that preserve operation after failure. The word has a different formal role in a dispensable proof graph.

Scope of Application

The literal setting is a propositional resolution proof represented as a rooted DAG whose leaves are input clauses and whose internal nodes are resolution inferences. In that setting a proof can be checked for validity and its total nodes counted. The cited paper studies ways to compress such proofs and defines redundancy by comparison with a smaller valid proof.[1]

The two worked positive settings are a finite local refutation rewrite and a parametric eager-unit refutation family.[1] They are unlike proof configurations, yet both satisfy the same root, validity, and strict-size tests.[1] Neither case licenses a blanket claim about informal mathematics, proof assistants with different inference rules, or the prevalence of redundancy in actual solver logs.

Clarity

The formal criterion resolves an ambiguity in “this proof has unnecessary steps.” Does that mean a repeated symbol is visible, a named rewrite applies, or a smaller proof actually exists? Only the last, with validity, root subsumption, and node count checked, establishes the property in this entry.[1]

The distinction matters in Example 6. Its syntactic arrangement meets a potential global-redundancy pattern, but the three forms of replacement specified there do not yield a valid resolution step.[1] That is evidence against those replacements, not a proof that no alternative derivation can be shorter. The frozen source's broader “locally redundant” phrasing is therefore not carried into this entry.[1]

Manages Complexity

A resolution proof can contain many shared and repeated subderivations. The four-role test reduces the comparison to two checkable objects and two relations: original versus alternative proof, validity and root relation, then total-node inequality. It prevents a search heuristic from being confused with a positive witness and keeps the size metric explicit.[1]

That simplification is conceptual rather than an efficient decision algorithm. Finding a smaller proof may be difficult, and failing to find one with a named rewriting rule does not settle the existential question. The paper develops particular local and global compression techniques, but the property of redundancy is broader than any one such technique.[1]

Abstract Reasoning

Let P be the original rooted resolution DAG from a fixed clause set C, with root clause r(P) and node count |P|. A positive witness is another valid resolution DAG Q from C for which r(Q) equals or subsumes r(P) and |Q| < |P|. The notation restates the paper's node-count criterion while making this entry's fixed-input comparison explicit; it is not an added theorem.[1]

To reason about a proposed simplification, first verify every alternative inference. Then compare roots, then count all nodes. In Theorem 10's n = 3 instance, the eager refutation has six resolution inferences and four input-clause nodes, while LowerUnits has three inferences and the same four inputs: 10 versus 7 total nodes.[1] The numbers are derived from the theorem's inference counts and displayed input set, not quoted as a measured solver result.[1]

Knowledge Transfer

The criterion transfers within propositional resolution from a nearby local rewrite to a distributed eager-unit family: the clauses and proof shapes change, while the witness contract remains fixed. In Example 4, the saving is visible in a small drawn refutation.[1] In Theorem 10, the saving scales with the family parameter because repeated unit inferences accumulate across branches.[1]

One can ask a similar “is there a valid smaller witness?” question in other formal systems, but the answer would require that system's inference rules, notion of equivalent conclusion, premise policy, and size metric. This entry does not transfer the resolution-DAG result merely by reusing the word redundant.

Examples

Canonical: local refutation rewrite

Fontaine and colleagues' Example 4 draws two nearby original resolution refutations, ψ1 and ψ2, and a shorter rewritten refutation ψ3.[1] Both originals and the replacement derive the empty clause from the displayed premises.[1] The two original drawings are variants of one local setting; they are not being counted as two independent applications.[1]

Mapped back: original proof and fixed premise set → either displayed original and its input clauses; root-conclusion contract → both original and replacement refute to the empty clause; valid alternative witness → the drawn ψ3 derivation; strict total-node comparison → fewer nodes in ψ3 than in either displayed original.[1]

Applied: eager-unit refutation family

Theorem 10 constructs a family Sₙ for which eager unit-resolution refutations repeat unit work.[1] Its LowerUnits alternative uses n resolution inferences where the eager construction uses n(n+1)/2.[1] Both use the same n+1 input-clause nodes and refute to the empty clause.[1] For n = 3, counting all proof-DAG nodes yields 10 versus 7.[1] This is an analytic toy family; the authors do not present it as a measured run of a production solver.[1]

Mapped back: original proof and fixed premise set → eager refutation of S_3 and its four inputs; root-conclusion contract → empty-clause refutation in both cases; valid alternative witness → the LowerUnits construction; strict total-node comparison → 10 eager nodes versus 7 LowerUnits nodes.[1]

Structural Tensions

The cited source establishes a formal property and specific rewrite comparisons. It does not establish a general pair of competing objectives that is necessary to this property's identity. A smaller valid proof is the positive criterion, and an equal-size or invalid alternative simply fails it. A heuristic that saves search time while missing a possible reduction could create an implementation trade-off, but the two checked examples do not quantify such a trade-off. Diagnostic: Is the claim about an actual smaller valid proof, or only about a method's ability to find one?[1]

Structural–Framed Character

This is mostly structural within a formal proof system. Its conclusion is checkable once the original and alternative DAGs, root clauses, premise set, and node-count measure are specified. Its evaluative weight lies in the chosen size metric and the requirement for a strict saving; those are explicit formal conventions rather than a human judgment that one proof “feels repetitive.”[1]

Human practice enters in selecting a proof representation and compression objective. The concept's institutional origin is automated-reasoning research, where proof graphs can be stored, transformed, and checked. Its technical vocabulary travels among resolution proofs because the same inference rule and DAG semantics hold there; applying the name to an informal proof would import an analogy until an appropriate validity and size contract is defined. The portable relation is a valid smaller substitute for a specified formal object, but the named property retains resolution-specific clauses, subsumption, and graph nodes. Its character: a formally testable property inside propositional resolution, with a potentially wider pattern that this evidence does not yet establish as a Prime.

Structural Core vs. Domain Accent

The core is a valid proof DAG, a conclusion-preserving alternative, and a strict node-count reduction under fixed inputs. The precise clause labels, pivots, and whether repeated work is local or distributed are accents of the two demonstrated proof configurations.[1] Change the size measure or inference system and the criterion has to be specified anew; deleting repeated-looking nodes without verifying the resulting proof does not preserve the core.

This entry remains domain-specific because resolution inferences, clause subsumption, and DAG-node counts do real definitional work. The catalog's Compression Prime is related through the aim of a shorter representation, but a redundant proof is a property of an original proof under an existential alternative, not itself a compression operation. The portable smaller-valid-substitute relation is a future-Prime question: it would need unlike formal systems and a shared invariant with explicit validity and size semantics before becoming a cross-domain catalog identity.

Compression is relevant when a valid shorter proof is actually constructed, because the result occupies fewer proof nodes under the selected metric. The live Resolution Proof Compression by Splitting entry names a particular procedure for producing a candidate smaller refutation; this property does not require splitting or any other single algorithm.

The live Redundancy Prime has a different meaning: it retains duplicate components for fault tolerance. Removing dispensable proof work is not an instance of that safety architecture. A typed parent, if one exists, must be justified by the proof property's necessary structure rather than the title's word match.

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

Computed from structural-signature embeddings · 2026-10-25

Not to Be Confused With

  • A repeated clause or pivot: a possible clue for a rewrite, not a proof that a smaller valid alternative exists.[1]
  • Failure of Definition 5's three rewrites: a bounded negative result in Example 6, not proof of absolute minimality.[1]
  • Resolution Proof Compression by Splitting: a specific split-and-recombine algorithm, whereas redundancy is the tested existence of any smaller valid proof meeting the conclusion contract.
  • The fault-tolerance Redundancy Prime: deliberate spare components, not excess steps in a resolution derivation.
  • A shorter derivation from new premises: a changed input problem, excluded by this entry's declared comparison 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 the proof-DAG definition and node measure (printed pp.238–239), Definition 3 and Example 4 (pp.239–240), Definition 5 and Example 6 (p.240), and Theorem 10 (p.243). The n = 3 total-node comparison is derived from the theorem's inference counts plus its displayed input clauses. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y ↩z ↩27 ↩28 ↩29 ↩30 ↩31 ↩32 ↩33 ↩34 ↩35 ↩36 ↩37 ↩38