{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T07:43:18Z","timestamp":1777534998806,"version":"3.51.4"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1988,3,1]],"date-time":"1988-03-01T00:00:00Z","timestamp":573177600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch Math Logic"],"published-print":{"date-parts":[[1988,3]]},"DOI":"10.1007\/bf01625836","type":"journal-article","created":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:25:39Z","timestamp":1114907139000},"page":"69-84","source":"Crossref","is-referenced-by-count":57,"title":["The number of proof lines and the size of proofs in first order logic"],"prefix":"10.1007","volume":"27","author":[{"given":"Jan","family":"Kraj\u00ed\u010dek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"Pudl\u00e1k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Symbolic logic and mechanical theorem proving","author":"C.-L. Chang","year":"1973","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. New York and London: Academic Press 1973"},{"key":"CR2","unstructured":"Farmer, W.M.: Length of proofs and unification theory. Ph. D. thesis, Univ. of Wisconsin-Madison, 1984"},{"key":"CR3","unstructured":"Farmer, W.M.: A unification-theoretic method for investigating thek-provability problem, preprint, 1987"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci.13, 225\u2013230 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"CR5","unstructured":"Kraj\u00ed\u010dek, J.: On the number of steps in proofs, submitted to Ann. Pure Appl. Logic, 1985"},{"key":"CR6","volume-title":"Generalizations of proofs, to appear in the Proc. 5th Easter Conf. on Model Th.","author":"J. Kraj\u00ed\u010dek","year":"1987","unstructured":"Kraj\u00ed\u010dek, J.: Generalizations of proofs, to appear in the Proc. 5th Easter Conf. on Model Th., Humboldt-Univ., Berlin (1987)"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"115","DOI":"10.21099\/tkbjm\/1496158798","volume":"4","author":"T. Miyatake","year":"1980","unstructured":"Miyatake, T.: On the length of proofs in formal systems. Tsukuba J. Math.4, 115\u2013125 (1980)","journal-title":"Tsukuba J. Math."},{"key":"CR8","unstructured":"Orevkov, V.P.: Reconstitution of the proof from its scheme (Russian abstract), 8th Sov. Conf. Math. Log., Novosibirsk 1984, p. 133"},{"key":"CR9","first-page":"87","volume":"137","author":"V.P. Orevkov","year":"1984","unstructured":"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\u201398, Leningrad (1984)","journal-title":"Theor. compl. of Comp., ser. Notes of Sci. sem. of Leningrad dept. of Math. Inst. Acad. Sci."},{"issue":"2","key":"CR10","first-page":"313","volume":"293","author":"V.P. Orevkov","year":"1987","unstructured":"Orevkov, V.P.: Reconstruction of a proof by its analysis (Russian). Doklady Akad. Nauk293 (2), 313\u2013316 (1987)","journal-title":"Doklady Akad. Nauk"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. Parikh","year":"1973","unstructured":"Parikh, R.: Some results on the length of proofs.TAMS 177, 29\u201336 (1973)","journal-title":"TAMS"},{"key":"CR12","first-page":"1","volume-title":"7th Int. Conf. on Autom. Deduct., LN in Comp. Sci., No. 170","author":"J. Siekman","year":"1984","unstructured":"Siekman, J.: Universal unification. In: Shostuk, R.E. (ed.), 7th Int. Conf. on Autom. Deduct., LN in Comp. Sci., No. 170, pp. 1\u201342. Berlin: Springer 1984"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0003-4843(78)90011-6","volume":"15","author":"R. Statman","year":"1978","unstructured":"Statman, R.: Bounds for proof-search and speed-up in the predicate calculus. Ann. Math. Logic15, 225\u2013287 (1978)","journal-title":"Ann. Math. Logic"},{"key":"CR14","unstructured":"Takeuti, G.: Proof theory. North-Holland 1975"},{"key":"CR15","first-page":"195","volume":"6","author":"T. Yukami","year":"1984","unstructured":"Yukami, T.: Some results on speed-up. Ann. Jap. Assoc. Philos. Sci., Vol.6, 195\u2013205 (1984)","journal-title":"Ann. Jap. Assoc. Philos. Sci."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01625836.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01625836\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01625836","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,8]],"date-time":"2019-05-08T06:52:13Z","timestamp":1557298333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01625836"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1988,3]]}},"alternative-id":["BF01625836"],"URL":"https:\/\/doi.org\/10.1007\/bf01625836","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988,3]]}}}