{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:04:10Z","timestamp":1743149050706,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_32","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"438-442","source":"Crossref","is-referenced-by-count":2,"title":["Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Generic Architecture for Proofs (GAPT), \n                      http:\/\/code.google.com\/p\/gapt\/"},{"key":"32_CR2","unstructured":"Sledgehammer, \n                      http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/sledgehammer.html"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-56992-8_4","volume-title":"Computer Science Logic","author":"M. Baaz","year":"1993","unstructured":"Baaz, M., Zach, R.: Algorithmic Structuring of Cut-free Proofs. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 29\u201342. Springer, Heidelberg (1993)"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-14203-1_36","volume-title":"Automated Reasoning","author":"T. Dunchev","year":"2010","unstructured":"Dunchev, T., Leitsch, A., Libal, T., Weller, D., Woltzenlogel Paleo, B.: System Description: The Proof Transformation System CERES. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 427\u2013433. Springer, Heidelberg (2010)"},{"key":"32_CR5","series-title":"Beyond Words","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-59126-6_1","volume-title":"Handbook of Formal Languages","author":"F. G\u00e9cseg","year":"1997","unstructured":"G\u00e9cseg, F., Steinby, M.: Tree Languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages. Beyond Words, vol.\u00a03, pp. 1\u201368. Springer, Heidelberg (1997)"},{"issue":"2","key":"32_CR6","first-page":"176","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen I. Mathematische Zeitschrift\u00a039(2), 176\u2013210 (1934)","journal-title":"Mathematische Zeitschrift"},{"key":"32_CR7","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. thesis, Universit\u00e9 de Paris (1930)"},{"key":"32_CR8","unstructured":"Hetzl, S.: Proofs as Tree Languages, submitted, preprint, \n                      http:\/\/hal.archives-ouvertes.fr\/hal-00613713\/"},{"issue":"5","key":"32_CR9","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/s00153-010-0186-7","volume":"49","author":"S. Hetzl","year":"2010","unstructured":"Hetzl, S.: On the form of witness terms. Archive for Mathematical Logic\u00a049(5), 529\u2013554 (2010)","journal-title":"Archive for Mathematical Logic"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-28332-1_26","volume-title":"Language and Automata Theory and Applications","author":"S. Hetzl","year":"2012","unstructured":"Hetzl, S.: Applying Tree Languages in Proof Theory. In: Dediu, A.H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol.\u00a07183, pp. 301\u2013312. Springer, Heidelberg (2012)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-28717-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Hetzl","year":"2012","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards Algorithmic Cut-Introduction. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 228\u2013242. Springer, Heidelberg (2012)"},{"key":"32_CR12","unstructured":"Hetzl, S., Stra\u00dfburger, L.: Herbrand-Confluence for Cut-Elimination in Classical First-Order Logic (submitted)"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-642-00982-2_38","volume-title":"Language and Automata Theory and Applications","author":"F. Jacquemard","year":"2009","unstructured":"Jacquemard, F., Klay, F., Vacher, C.: Rigid Tree Automata. In: Dediu, A.H., Ionescu, A.M., Mart\u00edn-Vide, C. (eds.) LATA 2009. LNCS, vol.\u00a05457, pp. 446\u2013457. Springer, Heidelberg (2009)"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1016\/j.ic.2010.11.015","volume":"209","author":"F. Jacquemard","year":"2011","unstructured":"Jacquemard, F., Klay, F., Vacher, C.: Rigid tree automata and applications. Information and Computation\u00a0209, 486\u2013512 (2011)","journal-title":"Information and Computation"},{"key":"32_CR15","unstructured":"McGuire, G., Tugemann, B., Civario, G.: There is no 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem, \n                      http:\/\/arxiv.org\/abs\/1201.0749"},{"issue":"4","key":"32_CR16","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D. Miller","year":"1987","unstructured":"Miller, D.: A Compact Representation of Proofs. Studia Logica\u00a046(4), 347\u2013370 (1987)","journal-title":"Studia Logica"},{"issue":"4","key":"32_CR17","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: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-642-17511-4_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Vysko\u010dil","year":"2010","unstructured":"Vysko\u010dil, J., Stanovsk\u00fd, D., Urban, J.: Automated Proof Compression by Invention of New Definitions. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 447\u2013462. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T02:41:07Z","timestamp":1676774467000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}