{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T10:04:33Z","timestamp":1751882673108},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600176"},{"type":"electronic","value":"9783540494041"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022250","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:12:29Z","timestamp":1132621949000},"page":"106-120","source":"Crossref","is-referenced-by-count":3,"title":["Semi-unification and generalizations of a particularly simple form"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Salzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"8_CR1","unstructured":"Baaz, M. Note on the existence of most general semi-unifiers. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Kraj\u00ed\u010dek, editors, pp. 20\u201329. Oxford University Press, 1993."},{"key":"8_CR2","unstructured":"Baaz, M. and P. Pudl\u00e1k. Kreisel's conjecture for L\u22031. In Arithmetic, Proof Theory and Computational Complexity, P. Clote and J. Kraj\u00ed\u010dek, editors, pp. 30\u201360. Oxford University Press, 1993."},{"key":"8_CR3","unstructured":"Chang, C.-L. and Lee, R.C.-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"W. M. Farmer","year":"1988","unstructured":"Farmer, W. M. A unification algorithm for second-order monadic terms. In Ann. Pure Appl. Logic, 39 (1988), 131\u2013174.","journal-title":"Ann. Pure Appl. Logic"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J. Kraj\u00ed\u010dek","year":"1988","unstructured":"Kraj\u00ed\u010dek, J. and P. Pudl\u00e1k. The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic, 27 (1988), 69\u201384.","journal-title":"Arch. Math. Logic"},{"key":"8_CR6","unstructured":"Kreisel, G. Generalizing Proofs: Implications for Generalizing Theorems Proved in Relatively Few Lines, I. Unpublished manuscript."},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1006\/inco.1993.1003","volume":"102","author":"A. Kfoury","year":"1993","unstructured":"Kfoury, A., J. Tiuryn, and P. Urzyczyn. The undecidability of the semiunification problem. Information and Computation, 102 (1993), 83\u2013101.","journal-title":"Information and Computation"},{"issue":"2","key":"8_CR8","first-page":"147","volume":"103","author":"G. S. Makanin","year":"1977","unstructured":"Makanin, G. S. The problem of solvability of equations in a free semigroup. Mat. Sb., 103(2), 147\u2013236. English translation in Math. USSR Sb., 32 (1977).","journal-title":"Mat. Sb."},{"key":"8_CR9","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"R. J. Parikh","year":"1973","unstructured":"Parikh, R. J. Some results on the length of proofs. Trans. Am. Math. Soc., 177 (1973), 29\u201336.","journal-title":"Trans. Am. Math. Soc."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Richardson, D. Sets of theorems with short proofs. J. Symbolic Logic, 39(2), 235\u2013242.","DOI":"10.2307\/2272636"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:12:52Z","timestamp":1554570772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0022250","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}