Article PDF
Avoid common mistakes on your manuscript.
References
Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. New York and London: Academic Press 1973
Farmer, W.M.: Length of proofs and unification theory. Ph. D. thesis, Univ. of Wisconsin-Madison, 1984
Farmer, W.M.: A unification-theoretic method for investigating thek-provability problem, preprint, 1987
Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci.13, 225–230 (1981)
Krajíček, J.: On the number of steps in proofs, submitted to Ann. Pure Appl. Logic, 1985
Krajíček, J.: Generalizations of proofs, to appear in the Proc. 5th Easter Conf. on Model Th., Humboldt-Univ., Berlin (1987)
Miyatake, T.: On the length of proofs in formal systems. Tsukuba J. Math.4, 115–125 (1980)
Orevkov, V.P.: Reconstitution of the proof from its scheme (Russian abstract), 8th Sov. Conf. Math. Log., Novosibirsk 1984, p. 133
Orevkov, V.P.: Upper bounds for lengthening of proofs after cut-elimination (Russian). In: Theor. compl. of Comp., ser. Notes of Sci. sem. of Leningrad dept. of Math. Inst. Acad. Sci.137, pp. 87–98, Leningrad (1984)
Orevkov, V.P.: Reconstruction of a proof by its analysis (Russian). Doklady Akad. Nauk293 (2), 313–316 (1987)
Parikh, R.: Some results on the length of proofs.TAMS 177, 29–36 (1973)
Siekman, J.: Universal unification. In: Shostuk, R.E. (ed.), 7th Int. Conf. on Autom. Deduct., LN in Comp. Sci., No. 170, pp. 1–42. Berlin: Springer 1984
Statman, R.: Bounds for proof-search and speed-up in the predicate calculus. Ann. Math. Logic15, 225–287 (1978)
Takeuti, G.: Proof theory. North-Holland 1975
Yukami, T.: Some results on speed-up. Ann. Jap. Assoc. Philos. Sci., Vol.6, 195–205 (1984)
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Krajíček, J., Pudlák, P. The number of proof lines and the size of proofs in first order logic. Arch Math Logic 27, 69–84 (1988). https://doi.org/10.1007/BF01625836
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01625836