{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:58:48Z","timestamp":1725562728591},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152047"},{"type":"electronic","value":"9783642152054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15205-4_28","type":"book-chapter","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T14:48:24Z","timestamp":1281710904000},"page":"351-365","source":"Crossref","is-referenced-by-count":2,"title":["A Sequent Calculus with Implicit Term Representation"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"28_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem Proving via General Matings. Journal of the ACM\u00a028(2), 193\u2013214 (1981)","journal-title":"Journal of the ACM"},{"key":"28_CR2","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"The Optimal Implementation of Functional Programming Languages","author":"A. Asperti","year":"1998","unstructured":"Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol.\u00a045. Cambridge University Press, Cambridge (1998)"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning","author":"F. Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification Theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013533. Elsevier, Amsterdam (2001)"},{"key":"28_CR4","unstructured":"Baaz, M., Hetzl, S.: On the non-confluence of cut-elimination. To appear in the Journal of Symbolic Logic (preprint), \n                    \n                      http:\/\/www.logic.at\/people\/hetzl\/"},{"issue":"2-3","key":"28_CR5","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"},{"issue":"2","key":"28_CR6","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":"3","key":"28_CR7","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.B., Schellinx, H.: A New Deconstructive Logic: Linear Logic. Journal of Symbolic Logic\u00a062(3), 755\u2013807 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"28_CR8","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031, 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"28_CR9","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"28_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0168-0072(91)90015-E","volume":"51","author":"W.M. Farmer","year":"1991","unstructured":"Farmer, W.M.: A unification-theoretic method for investigating the k-provability problem. Annals of Pure and Applied Logic\u00a051, 173\u2013214 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"28_CR11","series-title":"Beyond Words","first-page":"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":"3","key":"28_CR12","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1017\/S0960129507006123","volume":"17","author":"H. Geuvers","year":"2007","unstructured":"Geuvers, H., Loeb, I.: Natural Deduction via Graphs: Formal Definition and Computation Rules. Mathematical Structures in Computer Science\u00a017(3), 485\u2013526 (2007)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"28_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2008.03.036","volume":"203","author":"H. Geuvers","year":"2008","unstructured":"Geuvers, H., Loeb, I.: Deduction Graphs with Universal Quantification. Electronic Notes in Theoretical Computer Science\u00a0203(1), 93\u2013108 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"28_CR14","volume-title":"Proof Theory and Logical Complexity","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Proof Theory and Logical Complexity. Elsevier, Amsterdam (1987)"},{"issue":"2","key":"28_CR15","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a013(2), 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"28_CR16","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"},{"issue":"1-2","key":"28_CR17","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.apal.2008.10.010","volume":"159","author":"S. Hetzl","year":"2009","unstructured":"Hetzl, S.: Describing proofs by short tautologies. Annals of Pure and Applied Logic\u00a0159(1-2), 129\u2013145 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"key":"28_CR18","unstructured":"Huet, G.: A Mechanization of Type Theory. In: Third Interational Joint Conference on Articifical Intelligence (IJCAI), pp. 139\u2013146 (1973)"},{"issue":"3:1","key":"28_CR19","first-page":"1","volume":"5","author":"D. Kesner","year":"2009","unstructured":"Kesner, D.: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science\u00a05(3:1), 1\u201329 (2009)","journal-title":"Logical Methods in Computer Science"},{"key":"28_CR20","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., Pudl\u00e1k, P.: The Number of Proof Lines and the Size of Proofs in First Order Logic. Archive for Mathematical Logic\u00a027, 69\u201384 (1988)","journal-title":"Archive for Mathematical Logic"},{"issue":"1-2","key":"28_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic\u00a051(1-2), 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"28_CR22","first-page":"313","volume":"293","author":"V. Orevkov","year":"1987","unstructured":"Orevkov, V.: Reconstruction of a proof by its analysis (russian). Doklady Akademii Nauk\u00a0293(3), 313\u2013316 (1987)","journal-title":"Doklady Akademii Nauk"},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"issue":"1","key":"28_CR24","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"28_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"Zucker, J.: The Correspondence Between Cut-Elimination and Normalization. Annals of Mathematical Logic\u00a07, 1\u2013112 (1974)","journal-title":"Annals of Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15205-4_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:02:30Z","timestamp":1606186950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15205-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152047","9783642152054"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15205-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}