{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T11:56:15Z","timestamp":1773143775521,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642175107","type":"print"},{"value":"9783642175114","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17511-4_25","type":"book-chapter","created":{"date-parts":[[2010,12,7]],"date-time":"2010-12-07T06:24:40Z","timestamp":1291703080000},"page":"447-462","source":"Crossref","is-referenced-by-count":10,"title":["Automated Proof Compression by Invention of New Definitions"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"first","affiliation":[]},{"given":"David","family":"Stanovsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1006\/jabr.1998.7467","volume":"208","author":"I. Dahn","year":"1998","unstructured":"Dahn, I.: Robbins algebras are boolean: A revision of mccune\u2019s computer-generated solution of robbins problem. Journal of Algebra\u00a0208(2), 526\u2013532 (1998)","journal-title":"Journal of Algebra"},{"key":"25_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol.\u00a05081, p. 333. Springer, Heidelberg (2008)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"Graf, P.: Term Indexing. LNCS, vol.\u00a01053. Springer, Heidelberg (1996)"},{"issue":"4","key":"25_CR4","first-page":"681","volume":"9","author":"A. Grabowski","year":"2001","unstructured":"Grabowski, A.: Robbins algebras vs. boolean algebras. Formalized Mathematics\u00a09(4), 681\u2013690 (2001)","journal-title":"Formalized Mathematics"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-61532-6_34","volume-title":"PRICAI \u201996: Topics in Artificial Intelligence","author":"X. Huang","year":"1996","unstructured":"Huang, X.: Translating machine-generated resolution proofs into nd-proofs at the assertion level. In: Foo, N.Y., G\u00f6bel, R. (eds.) PRICAI 1996. LNCS, vol.\u00a01114, pp. 399\u2013410. Springer, Heidelberg (1996)"},{"issue":"3","key":"25_CR6","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. Autom. Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"25_CR7","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"25_CR9","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: FLAIRS Conference, pp. 49\u201354 (2006)"},{"key":"25_CR10","first-page":"153","volume":"5","author":"G.D. Plotkin","year":"1969","unstructured":"Plotkin, G.D.: A note on inductive generalization. Machine Intelligence\u00a05, 153\u2013163 (1969)","journal-title":"Machine Intelligence"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0304-3975(94)00227-A","volume":"142","author":"M. Proietti","year":"1995","unstructured":"Proietti, M., Pettorossi, A.: Unfolding\u2013definition\u2013folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science\u00a0142(1), 89\u2013124 (1995)","journal-title":"Theoretical Computer Science"},{"key":"25_CR12","unstructured":"Phillips, J.D., Stanovsk\u00fd, D.: Automated theorem proving in loop theory. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) ESARM: Empirically Successful Automated Reasoning in Mathematics. CEUR Workshop Proceedings, vol.\u00a0378, pp. 54\u201354. CEUR (2008)"},{"issue":"2-3","key":"25_CR13","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. Journal of AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"issue":"4","key":"25_CR14","first-page":"541","volume":"49","author":"D. Stanovsk\u00fd","year":"2008","unstructured":"Stanovsk\u00fd, D.: Distributive groupoids are symmetric-by-medial: An elementary proof. Commentationes Mathematicae Universitatis Carolinae\u00a049(4), 541\u2013546 (2008)","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"issue":"4","key":"25_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The tptp problem library and associated infrastructure. J. Autom. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR16","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"109","volume-title":"UITP 2006","author":"S. Trac","year":"2007","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An interactive derivation viewer. In: UITP 2006. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 109\u2013123. Elsevier, Amsterdam (2007)"},{"key":"25_CR17","unstructured":"Tamaki, H., Sato, T.: Unfold\/fold transformations of logic programs. In: T\u00e4rnlund, S.-\u00c5. (ed.) Proceedings of The Second International Conference on Logic Programming, pp. 127\u2013139 (1984)"},{"key":"25_CR18","unstructured":"Urban, J.: Automated reasoning for mizar: Artificial intelligence through knowledge exchange. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR Workshops. CEUR Workshop Proceedings, vol.\u00a0418. CEUR-WS.org (2008)"},{"key":"25_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: Malarea sg1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"issue":"2","key":"25_CR20","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1010639725972","volume":"27","author":"R. Veroff","year":"2001","unstructured":"Veroff, R.: Solving open questions and other challenge problems using proof sketches. J. Autom. Reasoning\u00a027(2), 157\u2013174 (2001)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-76631-5_29","volume-title":"MICAI 2007: Advances in Artificial Intelligence","author":"J. Vysko\u010dil","year":"2007","unstructured":"Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: Improving efficiency of prolog programs by fully automated unfold\/fold transformation. In: Gelbukh, A., Kuri Morales, \u00c1.F. (eds.) MICAI 2007. LNCS (LNAI), vol.\u00a04827, pp. 305\u2013315. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17511-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T17:53:47Z","timestamp":1553277227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17511-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642175107","9783642175114"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17511-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}