{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:27Z","timestamp":1758979287502},"reference-count":39,"publisher":"Oxford University Press (OUP)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1093\/logcom\/exu030","type":"journal-article","created":{"date-parts":[[2014,6,7]],"date-time":"2014-06-07T03:12:54Z","timestamp":1402110774000},"page":"577-603","source":"Crossref","is-referenced-by-count":14,"title":["A multi-focused proof system isomorphic to expansion proofs"],"prefix":"10.1093","volume":"26","author":[{"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2014,6,6]]},"reference":[{"key":"2016032907475279000_26.2.577.1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"2016032907475279000_26.2.577.2","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322249"},{"key":"2016032907475279000_26.2.577.3","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1294171002"},{"key":"2016032907475279000_26.2.577.4","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1333566645"},{"key":"2016032907475279000_26.2.577.5","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322277"},{"key":"2016032907475279000_26.2.577.6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_33"},{"key":"2016032907475279000_26.2.577.7","first-page":"383","article-title":"Canonical sequent proofs via multi-focusing","volume-title":"Fifth International Conference on Theoretical Computer Science","volume":"273","author":"Chaudhuri","year":"2008"},{"key":"2016032907475279000_26.2.577.8","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"2016032907475279000_26.2.577.9","doi-asserted-by":"crossref","unstructured":"Delande O. Miller D. A neutral approach to proof and refutation in MALL. In: Pfenning F. , editor. 23th Symp. on Logic in Computer Science. IEEE Computer Society Press; 2008. p. 498-508.","DOI":"10.1109\/LICS.2008.35"},{"key":"2016032907475279000_26.2.577.10","unstructured":"Felty A. Transforming specifications in a dependent-type lambda calculus to specifications in an intuitionistic logic. In: Huet G. Plotkin G. D. , editors. Logical Frameworks. Cambridge University Press; 1991."},{"key":"2016032907475279000_26.2.577.11","doi-asserted-by":"crossref","unstructured":"Gentzen G. Investigations into logical deduction. In: Szabo M. E. , editor. The Collected Papers of Gerhard Gentzen. North-Holland; 1969. p. 68-131. Translation of articles that appeared in 1934-35.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"2016032907475279000_26.2.577.12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2016032907475279000_26.2.577.13","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"2016032907475279000_26.2.577.14","unstructured":"Guglielmi A. Gundersen T. Parigot M. A proof calculus which reduces syntactic bureaucracy. In: Lynch C. , editor. Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010). Vol. 6. p. 135-150. of Leibniz International Proceedings in Informatics (LIPIcs) Edinburgh, United Kingdom, July 2010. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik."},{"key":"2016032907475279000_26.2.577.15","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.04.006"},{"key":"2016032907475279000_26.2.577.16","unstructured":"H. Herbelin and A. Saurin. \u03bb-calculus and \u039b-calculus: a capital difference. Unpublished manuscript, 2010."},{"key":"2016032907475279000_26.2.577.17","unstructured":"Herbrand J. Recherches sur la Th\u00e9orie de la D\u00e9monstration. University of Paris; 1930. PhD Thesis."},{"key":"2016032907475279000_26.2.577.18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28332-1_26"},{"key":"2016032907475279000_26.2.577.19","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-1716811"},{"key":"2016032907475279000_26.2.577.20","first-page":"320","article-title":"Herbrand-confluence for cut-elimination in classical first-order logic","volume-title":"Computer Science Logic (CSL) 2012","volume":"16","author":"Hetzl","year":"2012"},{"key":"2016032907475279000_26.2.577.21","unstructured":"Howe J. M. Proof Search Issues in Some Non-Classical Logics. University of St Andrews; 1998. PhD Thesis, Dec. Available as University of St Andrews Research Report CS\/99\/1."},{"key":"2016032907475279000_26.2.577.22","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2006.164.1065","article-title":"Proofs without syntax","volume":"143","author":"Hughes","year":"2006","journal-title":"Annals of Mathematics"},{"key":"2016032907475279000_26.2.577.23","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/11417170_19","article-title":"Naming proofs in classical propositional logic","volume-title":"Typed Lambda Calculi and Applications, TLCA 2005","volume":"3461","author":"Lamarche","year":"2005"},{"key":"2016032907475279000_26.2.577.24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-2(4:3)2006","article-title":"From proof nets to the free *-autonomous category","volume":"2","author":"Lamarche","year":"2006","journal-title":"Logical Methods in Computer Science"},{"key":"2016032907475279000_26.2.577.25","unstructured":"Lambek J. Scott P. J. Introduction to Higher Order Categorical Logic. Cambridge University Press; 1986."},{"key":"2016032907475279000_26.2.577.26","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"2016032907475279000_26.2.577.27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_38"},{"key":"2016032907475279000_26.2.577.28","doi-asserted-by":"crossref","unstructured":"McKinley R. Proof nets for Herbrand's theorem. ACM Transactions on Computational Logic 2013;14. To appear.","DOI":"10.1145\/2422085.2422090"},{"key":"2016032907475279000_26.2.577.29","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370646"},{"key":"2016032907475279000_26.2.577.30","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"2016032907475279000_26.2.577.31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_31"},{"key":"2016032907475279000_26.2.577.32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13962-8_37"},{"key":"2016032907475279000_26.2.577.33","unstructured":"Novakovi\u0107 N. S\u00e9mantique Alg\u00e9brique des Ressources pour la Logique Classique. Institut National Polytechnique de Lorraine; 2011. PhD Thesis."},{"key":"2016032907475279000_26.2.577.34","unstructured":"Prawitz D. Natural Deduction. Almqvist & Wiksell; 1965."},{"key":"2016032907475279000_26.2.577.35","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.777"},{"key":"2016032907475279000_26.2.577.36","unstructured":"Saurin A. >Une \u00e9tude logique du contr\u00f4le (appliqu\u00e9e \u00e0 la programmation fonctionnelle et logique). Ecole Polytechnique; 2008. PhD Thesis, Sept."},{"key":"2016032907475279000_26.2.577.37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13962-8_45"},{"key":"2016032907475279000_26.2.577.38","unstructured":"Urban C. Classical Logic and Computation. University of Cambridge; 2000. PhD Thesis."},{"key":"2016032907475279000_26.2.577.39","first-page":"123","article-title":"Strong normalisation of cut-elimination in classical logic","volume":"45","author":"Urban","year":"2001","journal-title":"Fundamenta Informaticae"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/26\/2\/577\/7949908\/exu030.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T10:09:44Z","timestamp":1565518184000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exu030"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,6]]},"references-count":39,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,3,29]]},"published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1093\/logcom\/exu030"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exu030","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6,6]]}}}