On a unification problem related to Kreisel's conjecture
Pudlák, Pavel
Commentationes Mathematicae Universitatis Carolinae, Tome 029 (1988), p. 551-556 / Harvested from Czech Digital Mathematics Library
Access to full text
Full (PDF)
Publié le : 1988-01-01
Classification:  03B25,  03B35,  03F07,  03F35,  03F99,  68T15 
@article{106669,
     author = {Pavel Pudl\'ak},
     title = {On a unification problem related to Kreisel's conjecture},
     journal = {Commentationes Mathematicae Universitatis Carolinae},
     volume = {029},
     year = {1988},
     pages = {551-556},
     zbl = {0664.03037},
     mrnumber = {972836},
     language = {en},
     url = {http://dml.mathdoc.fr/item/106669}
}

Pudlák, Pavel. On a unification problem related to Kreisel's conjecture. Commentationes Mathematicae Universitatis Carolinae, Tome 029 (1988) pp. 551-556. http://gdmltest.u-ga.fr/item/106669/

M. Baaz General solutions of equations with variables for substitutions, preprint.

M. Baaz Generalizing proofs with order-induction, manuscript.

M. Baaz , Personal communication. | Zbl 1157.03301

C.-L. Chang R. C.-T. Lee Symbolic logic and mechanical theorem proving, Chapter 5, New York and London, Academic Press 1973. (1973) | MR 0441028

W. M. Farmer Length of proofs and unification theory, Ph.D. thesis, Univ. of Wisconsin, Madison, 1984. (1984)

W. D. Goldfarb The undecidability of the second-order unification problem, Theor. Comput. Sci. 13 (1981), 225-230. (1981) | 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. (1988) | MR 0955313

V. P. Orevkov Reconstruction of a proof by its analysis, (Russian), Doklady Akad. Nauk 293 (1987), 313-316. (1987) | 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. (1984) | MR 0778038