Condensed Detachment¶
An inference rule that unifies an implication’s antecedent with a minor premise and detaches the most general resulting consequent.
Core Idea¶
Condensed detachment—also called rule D—combines uniform substitution and modus ponens into one inference operation. Given a major premise whose outer form is \(A\to B\) and a minor premise \(C\), first standardize variables apart, then compute a most general unifier \(\sigma\) of \(A\) and \(C\). If unification succeeds, infer \(\sigma(B)\), with any conventionally permitted variable normalization.
The word “condensed” refers to doing only the substitution needed to detach the consequent, while retaining a most-general result. Any more specialized conclusion obtainable from that application is a substitution instance of the condensed conclusion. Kalman formalized this rule using Robinson-style unification and proved a precise relationship with derivations using uniform substitution plus ordinary detachment.
Scope of Application¶
The rule belongs to implicational propositional calculi, equivalential calculi encoded as terms, single-axiom investigations, automated deduction, and the formula-as-types study of combinatory logic. It was proposed by Carew Meredith in the 1950s and later given rigorous unification-based formulations. Hindley and David Meredith relate rule D to principal type-scheme computation under the formulas-as-types correspondence.
Automated theorem provers use the rule as a compact inference kernel for search over axiom systems. McCune and Wos reported experiments on 112 condensed-detachment problems using the OTTER prover, varying search and deletion strategies. Such application evidence shows recurrence, not that D dominates every theorem-proving calculus.
Clarity¶
The abstraction clarifies where generality enters an inference. Ordinary presentations can first instantiate an axiom many ways and then detach. Rule D reverses that workflow: match the actual minor to the antecedent, compute only a most-general necessary substitution, and return the most-general detachable consequent.
Three checks prevent ambiguity. Variables from premises must be standardized apart so same spellings do not create accidental identity.
Manages Complexity¶
Rule D compresses two recurring proof steps—substitution and modus ponens—into one generative transition. Rather than enumerate infinitely many substitution instances of a theorem, a prover unifies on demand and keeps a conclusion that subsumes its specializations. This reduces representational redundancy and exposes the principal conclusion available from a premise pair.
Abstract Reasoning¶
Suppose \(A\to B\) and \(C\) are standardized apart. If \(\sigma\) is their most-general antecedent/minor unifier, then \(B\sigma\) represents all conclusions from that pair obtainable by first making compatible substitution instances and then applying modus ponens: any such more specific output factors through a further substitution. This is the principal-result invariant.
Knowledge Transfer¶
Literal transfer occurs between formal-logic calculi and automated proof engines when implication, substitution, and most-general unification preserve the same roles. The formulas-as-types correspondence supplies a rigorous adjacent transfer: condensed detachment corresponds to an algorithm for principal type schemes in combinatory logic, not merely a loose analogy.
Unification techniques transfer instrumentally from logic programming or type inference, but their host operations do not thereby become rule D. Outside formal symbolic systems, “detach after matching” is metaphorical unless terms, substitutions, most-generality, and consequent formation are defined.
Relationships to Other Abstractions¶
Current abstraction Condensed Detachment Domain-specific
Parents (1) — more general patterns this builds on
-
Condensed Detachment is a kind of Deductive Reasoning Prime
Condensed Detachment specializes Deductive Reasoning: it is a truth-preserving formal inference rule under its host calculus.
Hierarchy path (1) — routes to 1 parentless root
- Condensed Detachment → Deductive Reasoning
Neighborhood in Abstraction Space¶
Condensed Detachment sits in a sparse region of the domain-specific corpus (82nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Computational Number Theory & Enumeration (13 abstractions)
Nearest neighbors
- Variable Elimination — 0.83
- Transitive Set — 0.81
- Prime Model (Model Theory) — 0.81
- Classification of Discontinuities — 0.81
- Probabilistic Graphical Model — 0.81
Computed from structural-signature embeddings · 2026-09-08