{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T11:29:55Z","timestamp":1777548595564,"version":"3.51.4"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"unspecified","delay-in-days":37,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Herbrand\u2019s theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller\u2019s expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas.<\/jats:p><jats:p>In this paper, we present a new syntactic approach that directly extends Miller\u2019s expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.<\/jats:p>","DOI":"10.1017\/s0960129519000069","type":"journal-article","created":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T10:24:48Z","timestamp":1570530288000},"page":"1009-1029","source":"Crossref","is-referenced-by-count":4,"title":["Expansion trees with cut"],"prefix":"10.1017","volume":"29","author":[{"given":"Federico","family":"Aschieri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"S0960129519000069_ref26","first-page":"123","article-title":"Strong normalization of cut-elimination in classical logic","volume":"45","author":"Urban","year":"2000","journal-title":"Fundamenta Informaticae"},{"key":"S0960129519000069_ref25","unstructured":"Urban, C. (2000). Classical Logic and Computation. Phd thesis, University of Cambridge."},{"key":"S0960129519000069_ref24","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq011"},{"key":"S0960129519000069_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6610-7"},{"key":"S0960129519000069_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422090"},{"key":"S0960129519000069_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_14"},{"key":"S0960129519000069_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0960129519000069_ref10","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"S0960129519000069_ref16","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-1716811"},{"key":"S0960129519000069_ref6","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1999.0359"},{"key":"S0960129519000069_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_20"},{"key":"S0960129519000069_ref3","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1294171002"},{"key":"S0960129519000069_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129519000069_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00026-8"},{"key":"S0960129519000069_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370646"},{"key":"S0960129519000069_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2275524"},{"key":"S0960129519000069_ref18","volume-title":"Grundlagen der Mathematik II","author":"Hilbert","year":"1939"},{"key":"S0960129519000069_ref17","unstructured":"Hetzl, S. and Stra\u00dfburger, L. (2012). Herbrand-confluence for cut-elimination in classical first-order logic. In: C\u00e9gielski, P. and Durand, A. (eds.) Computer Science Logic (CSL) 2012, Leibniz International Proceedings in Informatics (LIPIcs), vol. 16, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 320\u2013334."},{"key":"S0960129519000069_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2016.48"},{"key":"S0960129519000069_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"S0960129519000069_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.028"},{"key":"S0960129519000069_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_32"},{"key":"S0960129519000069_ref7","volume-title":"Computer Science","author":"Buss","year":"1995"},{"key":"S0960129519000069_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.04.006"},{"key":"S0960129519000069_ref14","unstructured":"Heijltjes, W. (2011). Graphical Representation of Canonical Proof: Two Case Studies. Phd thesis, University of Edinburgh."},{"key":"S0960129519000069_ref15","unstructured":"Herbrand, J. (1930). Recherches sur la th\u00e9orie de la d\u00e9monstration. Phd thesis, Universit\u00e9 de Paris."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129519000069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T10:25:02Z","timestamp":1570530302000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129519000069\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":26,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129519000069"],"URL":"https:\/\/doi.org\/10.1017\/s0960129519000069","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}