Weaker D-complete logics
The condensed detachment rule, first proposed by C. A. Meredith in Lemmon et al , is a form of modus ponens preceded by 'just enough' substitution to make the modus ponens possible. The substitution mechanism, for implicational formulas, was a precursor to Robinson's unification algorithm .
Megill, N. D. & Bunder, M. W. (1996). Weaker D-complete logics. Logic Journal of the IGPL, 4 (2), 215-225.