{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:38:28Z","timestamp":1740141508059,"version":"3.37.3"},"reference-count":37,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2020,10,24]],"date-time":"2020-10-24T00:00:00Z","timestamp":1603497600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"publisher","award":["EP\/K018868\/1"],"award-info":[{"award-number":["EP\/K018868\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"ANR","doi-asserted-by":"publisher","award":["ANR-15-CE25-0014-01"],"award-info":[{"award-number":["ANR-15-CE25-0014-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,12,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The reduction of undecidable first-order logic to decidable propositional logic via Herbrand\u2019s theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. In this paper we construct simple deep inference systems for first-order logic, both with and without cut, such that \u2018decomposed\u2019 proofs\u2014proofs where the contractive and non-contractive behaviour of the proof is separated\u2014in each system correspond to either expansion proofs or Herbrand proofs. Translations between proofs in this system, expansion proofs and Herbrand proofs are given, retaining much of the structure in each direction.<\/jats:p>","DOI":"10.1093\/logcom\/exaa052","type":"journal-article","created":{"date-parts":[[2020,9,7]],"date-time":"2020-09-07T11:10:11Z","timestamp":1599477011000},"page":"1711-1742","source":"Crossref","is-referenced-by-count":1,"title":["Herbrand Proofs and Expansion Proofs as Decomposed Proofs"],"prefix":"10.1093","volume":"30","author":[{"given":"Benjamin","family":"Ralph","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Bath, Bath, Somerset, UK"}]}],"member":"286","published-online":{"date-parts":[[2020,10,24]]},"reference":[{"key":"2020120307172695600_ref1","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1017\/jsl.2018.51","article-title":"Unsound Inference Make Proofs Shorter","volume":"84","author":"Aguilera","year":"2019","journal-title":"The Journal of Symbolic Logic"},{"key":"2020120307172695600_ref2","first-page":"5:1","article-title":"The True Concurrency of Herbrand\u2019s Theorem","volume-title":"27th EACSL Annual Conference on Computer Science Logic (CSL 2018)","author":"Alcolei","year":"2018"},{"volume-title":"A Study of Normalisation through Subatomic Logic","year":"2017","author":"Tubella","key":"2020120307172695600_ref3"},{"key":"2020120307172695600_ref4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3173544","article-title":"Subatomic Proof Systems: Splittable Systems","volume":"19","author":"Tubella","year":"2018","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020120307172695600_ref5","first-page":"9:1","article-title":"Removing Cycles from Proofs","volume-title":"26th EACSL Annual Conference on Computer Science Logic (CSL 2017)","author":"Tubella","year":"2017"},{"key":"2020120307172695600_ref6","doi-asserted-by":"crossref","first-page":"1009","DOI":"10.1017\/S0960129519000069","article-title":"Expansion Trees with Cut","volume":"29","author":"Aschieri","year":"2018","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020120307172695600_ref7","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","article-title":"On skolemization and proof complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundamenta Informaticae"},{"volume-title":"Deep Inference and Symmetry in Classical Proofs","year":"2003","author":"Br\u00fcnnler","key":"2020120307172695600_ref8"},{"key":"2020120307172695600_ref9","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1093\/jigpal\/11.5.525","article-title":"Two restrictions on contraction","volume":"11","author":"Br\u00fcnnler","year":"2003","journal-title":"Logic Journal of IGPL"},{"key":"2020120307172695600_ref10","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/s11225-006-6605-4","article-title":"Cut elimination inside a deep inference system for classical predicate logic","volume":"82","author":"Br\u00fcnnler","year":"2006","journal-title":"Studia Logica"},{"key":"2020120307172695600_ref11","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45653-8_24","article-title":"A local system for classical logic","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Br\u00fcnnler","year":"2001"},{"key":"2020120307172695600_ref12","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-60178-3_85","article-title":"On Herbrand\u2019s theorem","volume-title":"Logic and Computational Complexity","author":"Buss","year":"1995"},{"key":"2020120307172695600_ref13","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1093\/logcom\/exu030","article-title":"A multi-focused proof system isomorphic to expansion proofs","volume":"26","author":"Chaudhuri","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"2020120307172695600_ref14","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-94-010-0630-9_4","article-title":"Kanger\u2019s choices in automated reasoning","volume-title":"Collected Papers of Stig Kanger with Essays on His Life and Work","author":"Degtyarev","year":"2001"},{"key":"2020120307172695600_ref15","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1090\/S0002-9904-1963-10990-8","article-title":"False lemmas in Herbrand","volume":"69","author":"Dreben","year":"1963","journal-title":"Bulletin of the American Mathematical Society"},{"key":"2020120307172695600_ref16","doi-asserted-by":"crossref","DOI":"10.1145\/1182613.1182614","article-title":"A system of interaction and structure","volume":"8","author":"Guglielmi","year":"2007","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020120307172695600_ref17","first-page":"135","article-title":"A Proof Calculus Which Reduces Syntactic Bureaucracy","volume-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA\u201910)","author":"Guglielmi","year":"2010"},{"key":"2020120307172695600_ref18","article-title":"A General View of Normalisation through Atomic Flows","volume-title":"PhD Thesis","author":"Gundersen","year":"2009"},{"key":"2020120307172695600_ref19","doi-asserted-by":"crossref","first-page":"1346","DOI":"10.1016\/j.apal.2010.04.006","article-title":"Classical proof forestry","volume":"161","author":"Heijltjes","year":"2010","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020120307172695600_ref20","article-title":"Recherches Sur La Th\u00e9orie de La D\u00e9monstration","volume-title":"PhD Thesis","author":"Herbrand","year":"1930"},{"key":"2020120307172695600_ref21","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-3072-4","volume-title":"Logical Writings","author":"Herbrand","year":"1971"},{"key":"2020120307172695600_ref22","first-page":"1878","article-title":"On the Infinite. Text of an address delivered in M\u00fcnster on 4th June 1925 at a meeting of the Westphalian Mathematical Society","volume-title":"Jean van Heijenoort","author":"Hilbert","year":"1967"},{"volume-title":"Grundlagen Der Mathematik II","year":"1974","author":"Hilbert","key":"2020120307172695600_ref23"},{"key":"2020120307172695600_ref24","first-page":"37","article-title":"Electronic Notes in Theoretical Computer Science","volume":"165","author":"Hughes","year":"2006","journal-title":"Towards Hilbert\u2019s 24th Problem: Combinatorial Proof Invariants (Preliminary version)"},{"article-title":"First-order proofs without syntax","year":"2019","author":"Hughes","key":"2020120307172695600_ref25"},{"key":"2020120307172695600_ref26","article-title":"Provability in logic","volume-title":"Stockholm studies in Philosophy","author":"Kanger","year":"1957"},{"key":"2020120307172695600_ref27","first-page":"585","article-title":"Sur une nouvelle classe de nombres transcendants","author":"Kuzmin","year":"1930","journal-title":"Bulletin de l\u2019Acad\u00e9mie des Sciences de l\u2019URSS. VII s\u00e9rie"},{"author":"McKinley","key":"2020120307172695600_ref28","article-title":"A sequent calculus demonstration of Herbrand\u2019s theorem"},{"key":"2020120307172695600_ref29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422085.2422090","article-title":"Proof nets for Herbrand\u2019s Theorem","volume":"14","author":"McKinley","year":"2013","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"2020120307172695600_ref30","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF00370646","article-title":"A compact representation of proofs","volume":"46","author":"Miller","year":"1987","journal-title":"Studia Logica"},{"key":"2020120307172695600_ref31","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/978-3-319-72056-2_18","article-title":"A Natural Proof System for Herbrand\u2019s Theorem","volume-title":"International Symposium on Logical Foundations of Computer Science","author":"Ralph","year":"2018"},{"volume-title":"Modular Normalisation of Classical Proofs","year":"2019","author":"Ralph","key":"2020120307172695600_ref32"},{"key":"2020120307172695600_ref33","first-page":"104","article-title":"Lower bounds on Herbrand\u2019s theorem","author":"Statman","year":"1979","journal-title":"Proceedings of the American Mathematical Society"},{"key":"2020120307172695600_ref34","article-title":"Combinatorial flows and their normalisation","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","author":"Stra\u00dfburger","year":"2017"},{"key":"2020120307172695600_ref35","article-title":"The problem of proof identity, and why computer scientists should care about Hilbert\u2019s 24th problem","volume":"377","author":"Stra\u00dfburger","year":"2019","journal-title":"Philosophical Transactions of the Royal Society A"},{"key":"2020120307172695600_ref36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1080\/00029890.2003.11919933","article-title":"Hilbert\u2019s twenty-fourth problem","volume":"110","author":"Thiele","year":"2003","journal-title":"American Mathematical Monthly"},{"volume-title":"On Herbrand\u2019s Theorem","year":"2014","author":"Webb","key":"2020120307172695600_ref37"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1711\/34673322\/exaa052.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/8\/1711\/34673322\/exaa052.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,3]],"date-time":"2020-12-03T12:22:07Z","timestamp":1606998127000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/8\/1711\/5937270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,24]]},"references-count":37,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2020,10,24]]},"published-print":{"date-parts":[[2020,12,10]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa052","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2020,12]]},"published":{"date-parts":[[2020,10,24]]}}}