{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:29:38Z","timestamp":1725748178680},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405365"},{"type":"electronic","value":"9783642405372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_15","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T08:33:51Z","timestamp":1378888431000},"page":"157-171","source":"Crossref","is-referenced-by-count":6,"title":["Understanding Resolution Proofs through Herbrand\u2019s Theorem"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[]},{"given":"Tomer","family":"Libal","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Riener","sequence":"additional","affiliation":[]},{"given":"Mikheil","family":"Rukhaia","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. PhD thesis, Universit\u00e9 de Paris (1930)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-60178-3_85","volume-title":"Logic and Computational Complexity","author":"S.R. Buss","year":"1995","unstructured":"Buss, S.R.: On Herbrand\u2019s Theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol.\u00a0960, pp. 195\u2013209. Springer, Heidelberg (1995)"},{"issue":"4","key":"15_CR3","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":"2","key":"15_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/jsco.1999.0359","volume":"29","author":"M. Baaz","year":"2000","unstructured":"Baaz, M., Leitsch, A.: Cut-elimination and Redundancy-elimination by Resolution. Journal of Symbolic Computation\u00a029(2), 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"234","DOI":"10.2307\/2275028","volume":"54","author":"H. Luckhardt","year":"1989","unstructured":"Luckhardt, H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. Journal of Symbolic Logic\u00a054(1), 234\u2013263 (1989)","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"15_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1017\/S1446788700030159","volume":"45","author":"E. Bombieri","year":"1988","unstructured":"Bombieri, E., van der Poorten, A.: Some quantitative results related to Roth\u2019s theorem. Journal of the Australian Mathematical Society\u00a045(2), 233\u2013248 (1988)","journal-title":"Journal of the Australian Mathematical Society"},{"key":"15_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-540-85110-3_38","volume-title":"Intelligent Computer Mathematics","author":"S. Hetzl","year":"2008","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand Sequent Extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC\/Calculemus\/MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 462\u2013477. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"15_CR8","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M. Baaz","year":"2008","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An Analysis of F\u00fcrstenberg\u2019s Proof of the Infinity of Primes. Theoretical Computer Science\u00a0403(2-3), 160\u2013175 (2008)","journal-title":"Theoretical Computer Science"},{"key":"15_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-540-32275-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Baaz","year":"2005","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Cut-Elimination: Experiments with CERES. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 481\u2013495. Springer, Heidelberg (2005)"},{"key":"15_CR10","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge (October 2000)"},{"key":"15_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. LNCS, vol.\u00a07180, pp. 228\u2013242. Springer, Heidelberg (2012)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-642-31374-5_32","volume-title":"Intelligent Computer Mathematics","author":"S. Hetzl","year":"2012","unstructured":"Hetzl, S.: Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 438\u2013442. Springer, Heidelberg (2012)"},{"key":"15_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48660-7_10","volume-title":"Automated Deduction - CADE-16","author":"H. Horacek","year":"1999","unstructured":"Horacek, H.: Presenting Proofs in a Human-Oriented Way. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 142\u2013156. Springer, Heidelberg (1999)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/10721959_37","volume-title":"Automated Deduction - CADE-17","author":"A. Meier","year":"2000","unstructured":"Meier, A.: System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 460\u2013464. Springer, Heidelberg (2000)"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.entcs.2006.09.025","volume":"174","author":"S. Trac","year":"2007","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An interactive derivation viewer. Electronic Notes in Theoretical Computer Science\u00a0174(2), 109\u2013123 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"15_CR16","unstructured":"Denzinger, J., Schulz, S.: Recording, Analyzing and Presenting Distributed Deduction Processes. In: Hong, H. (ed.) 1st International Symposium on Parallel Symbolic Computation (PASCO). Lecture Notes Series in Computing, vol.\u00a05, pp. 114\u2013123. World Scientific Publishing (1994)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-0-387-34768-4_23","volume-title":"7th International Conference on Automated Deduction","author":"F. Pfenning","year":"1984","unstructured":"Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol.\u00a0170, pp. 394\u2013413. Springer, Heidelberg (1984)"},{"key":"15_CR18","unstructured":"Pfenning, F.: Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University (1987)"},{"key":"15_CR19","unstructured":"Miller, D.: Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University (1983)"},{"issue":"2","key":"15_CR20","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":"15_CR21","unstructured":"Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Woltzenlogel-Paleo, B.: System Feature Description: Importing Refutations into the GAPT Framework. In: Proof Exchange for Theorem Proving Second International Workshop, PxTP (2012)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Mccune, W., Shumsky, O.: Ivy: A Preprocessor And Proof Checker For First-Order Logic. In: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0_16"},{"key":"15_CR23","unstructured":"McCune, W.: Prover9 and mace4 manual - output files (2005-2010), \n                    \n                      https:\/\/www.cs.unm.edu\/~mccune\/mace4\/manual\/2009-11A\/output.html"},{"issue":"4","key":"15_CR24","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":"15_CR25","unstructured":"Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Woltzenlogel-Paleo, B.: ProofTool: GUI for the GAPT Framework (to appear)"},{"key":"15_CR26","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T01:50:55Z","timestamp":1558057855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}