[1] M. BAAZ: General solutions of equations with variables for substitutions. preprint.
[2] M. BAAZ: Generalizing proofs with order-induction. manuscript.
[4] C.-L. CHANG R. C.-T. LEE:
Symbolic logic and mechanical theorem proving. Chapter 5, New York and London, Academic Press 1973.
MR 0441028
[5] W. M. FARMER: Length of proofs and unification theory. Ph.D. thesis, Univ. of Wisconsin, Madison, 1984.
[6] W. D. GOLDFARB:
The undecidability of the second-order unification problem. Theor. Comput. Sci. 13 (1981), 225-230.
MR 0594061 |
Zbl 0457.03006
[7] 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
[8] V. P. OREVKOV:
Reconstruction of a proof by its analysis. (Russian), Doklady Akad. Nauk 293 (1987), 313-316.
MR 0884040
[9] 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