M. BAAZ: General solutions of equations with variables for substitutions. preprint.
 M. BAAZ: Generalizing proofs with order-induction. manuscript.
 C.-L. CHANG R. C.-T. LEE: Symbolic logic and mechanical theorem proving
. Chapter 5, New York and London, Academic Press 1973. MR 0441028
 W. M. FARMER: Length of proofs and unification theory. Ph.D. thesis, Univ. of Wisconsin, Madison, 1984.
 W. D. GOLDFARB: The undecidability of the second-order unification problem
. Theor. Comput. Sci. 13 (1981), 225-230. MR 0594061
| Zbl 0457.03006
 J. KRAJÍČEK P. PUDLÁK: The number of proof lines and the size of proofs in first order logic
. Arch. Math. Logic 27 (1988), 69-84. MR 0955313
 V. P. OREVKOV: Reconstruction of a proof by its analysis
. (Russian), Doklady Akad. Nauk 293 (1987), 313-316. MR 0884040
 J. SIEKMAN: Universal unification. In: Shostuk, R. E. ed
. 7-th Int. Conf. on Autom. Deduction, LN in Comp. Sci. 170,1-42, Springer-Verlag 1984. MR 0778038