{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:23Z","timestamp":1740098963271,"version":"3.37.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319720555"},{"type":"electronic","value":"9783319720562"}],"license":[{"start":{"date-parts":[[2017,11,28]],"date-time":"2017-11-28T00:00:00Z","timestamp":1511827200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-72056-2_18","type":"book-chapter","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T04:33:31Z","timestamp":1511757211000},"page":"289-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Natural Proof System for Herbrand\u2019s Theorem"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5075-9360","authenticated-orcid":false,"given":"Benjamin","family":"Ralph","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,28]]},"reference":[{"unstructured":"Alcolei, A., Clairambault, P., Hyland, M., Winskel, G.: The true concurrency of Herbrand\u2019s theorem (2017, submitted)","key":"18_CR1"},{"unstructured":"Aler Tubella, A.: A study of normalisation through subatomic logic. University of Bath (2016)","key":"18_CR2"},{"doi-asserted-by":"crossref","unstructured":"Aler Tubella, A., Guglielmi, A.: Subatomic proof systems: splittable systems. arXiv preprint arXiv:1703.10258 (2017)","key":"18_CR3","DOI":"10.1145\/3173544"},{"unstructured":"Aler Tubella, A., Guglielmi, A., Ralph, B.: Removing cycles from proofs. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden 2017. Leibniz International Proceedings in Informatics (LIPIcs), pp. 9:1\u20139:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)","key":"18_CR4"},{"unstructured":"Br\u00fcnnler, K.: Deep inference and symmetry in classical proofs. Logos Verlag (2003)","key":"18_CR5"},{"issue":"5","key":"18_CR6","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1093\/jigpal\/11.5.525","volume":"11","author":"K Br\u00fcnnler","year":"2003","unstructured":"Br\u00fcnnler, K.: Two restrictions on contraction. Logic J. IGPL 11(5), 525\u2013529 (2003)","journal-title":"Logic J. IGPL"},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/s11225-006-6605-4","volume":"82","author":"K Br\u00fcnnler","year":"2006","unstructured":"Br\u00fcnnler, K.: Cut elimination inside a deep inference system for classical predicate logic. Stud. Logica. 82(1), 51\u201371 (2006)","journal-title":"Stud. Logica."},{"key":"18_CR8","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":"SR Buss","year":"1995","unstructured":"Buss, S.R.: On Herbrand\u2019s theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 195\u2013209. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60178-3_85"},{"issue":"2","key":"18_CR9","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1093\/logcom\/exu030","volume":"26","author":"K Chaudhuri","year":"2016","unstructured":"Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Logic Comput. 26(2), 577\u2013603 (2016). https:\/\/doi.org\/10.1093\/logcom\/exu030","journal-title":"J. Logic Comput."},{"doi-asserted-by":"publisher","unstructured":"Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (Rta 2010), vol. 6, pp. 135\u2013150 (2010). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.135","key":"18_CR10","DOI":"10.4230\/LIPIcs.RTA.2010.135"},{"unstructured":"Gundersen, T.E.: A general view of normalisation through atomic flows. University of Bath (2009)","key":"18_CR11"},{"issue":"11","key":"18_CR12","doi-asserted-by":"publisher","first-page":"1346","DOI":"10.1016\/j.apal.2010.04.006","volume":"161","author":"W Heijltjes","year":"2010","unstructured":"Heijltjes, W.: Classical proof forestry. Ann. Pure Appl. Logic 161(11), 1346\u20131366 (2010). https:\/\/doi.org\/10.1016\/j.apal.2010.04.006","journal-title":"Ann. Pure Appl. Logic"},{"key":"18_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-3072-4","volume-title":"Logical Writings","author":"J Herbrand","year":"1971","unstructured":"Herbrand, J., Goldfarb, W.D.: Logical Writings. Springer, Dordrecht (1971). https:\/\/doi.org\/10.1007\/978-94-010-3072-4"},{"unstructured":"Hetzl, S., Weller, D.: Expansion trees with cut. arXiv preprint arXiv:1308.0428 (2013)","key":"18_CR14"},{"unstructured":"McKinley, R.: A sequent calculus demonstration of Herbrand\u2019s theorem. arXiv preprint arXiv:1007.3414 (2010)","key":"18_CR15"},{"issue":"1","key":"18_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422085.2422090","volume":"14","author":"R McKinley","year":"2013","unstructured":"McKinley, R.: Proof nets for Herbrand\u2019s theorem. ACM Trans. Comput. Logic (TOCL) 14(1), 1\u201331 (2013). https:\/\/doi.org\/10.1145\/2422085.2422090","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"4","key":"18_CR17","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"DA Miller","year":"1987","unstructured":"Miller, D.A.: A compact representation of proofs. Stud. Logica. 46(4), 347\u2013370 (1987). https:\/\/doi.org\/10.1007\/BF00370646","journal-title":"Stud. Logica."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-02273-9_23","volume-title":"Typed Lambda Calculi and Applications","author":"L Stra\u00dfburger","year":"2009","unstructured":"Stra\u00dfburger, L.: Some observations on the proof theory of second order propositional multiplicative linear logic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 309\u2013324. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02273-9_23"},{"unstructured":"Stra\u00dfburger, L.: Deep inference, expansion trees, and proof graphs for second order propositional multiplicative linear logic, vol. RR-9071, p. 38. Inria Saclay Ile de France (2017)","key":"18_CR19"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72056-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T17:30:40Z","timestamp":1570383040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72056-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,28]]},"ISBN":["9783319720555","9783319720562"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72056-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,11,28]]}}}