{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T08:18:19Z","timestamp":1694852299838},"reference-count":40,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2019,6,4]],"date-time":"2019-06-04T00:00:00Z","timestamp":1559606400000},"content-version":"vor","delay-in-days":1,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,9,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Herbrand structures have the advantage, computationally speaking, of being guided by the definability of all elements in them. A salient feature of the logics induced by them is that they internally exhibit the induction scheme, thus providing a congenial, computationally oriented framework for formal inductive reasoning. Nonetheless, their enhanced expressivity renders any effective proof system for them incomplete. Furthermore, the fact that they are not compact poses yet another proof-theoretic challenge. This paper offers several layers for coping with the inherent incompleteness and non-compactness of these logics. First, two types of infinitary proof system are introduced\u2014one of infinite width and one of infinite height\u2014which manipulate infinite sequents and are sound and complete for the intended semantics. The restriction of these systems to finite sequents induces a completeness result for finite entailments. Then, in search of effectiveness, two finite approximations of these systems are presented and explored. Interestingly, the approximation of the infinite-width system via an explicit induction scheme turns out to be weaker than the effective cyclic fragment of the infinite-height system.<\/jats:p>","DOI":"10.1093\/logcom\/exz011","type":"journal-article","created":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T11:22:01Z","timestamp":1555413721000},"page":"693-721","source":"Crossref","is-referenced-by-count":2,"title":["Towards automated reasoning in Herbrand structures"],"prefix":"10.1093","volume":"29","author":[{"given":"Liron","family":"Cohen","sequence":"first","affiliation":[{"name":"Department of Computer Science, Cornell University , Ithaca NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reuben N S","family":"Rowe","sequence":"additional","affiliation":[{"name":"School of Computing, University of Kent, Canterbury , UK, NF"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[{"name":"Computer Science Department, Stanford University , Stanford CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2019,6,3]]},"reference":[{"key":"2019091313044445500_ref1","volume-title":"Foundations of Databases: The Logical Level","author":"Abiteboul","year":"1995"},{"key":"2019091313044445500_ref2","first-page":"455","article-title":"Argumentative approaches to reasoning with consistent subsets of premises","volume-title":"International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems","author":"Arieli","year":"2017"},{"key":"2019091313044445500_ref3","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-94-017-0253-9_7","article-title":"Transitive closure and the mechanization of mathematics","volume-title":"Thirty Five Years of Automating Mathematics","author":"Avron","year":"2003"},{"key":"2019091313044445500_ref4","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/LICS.2012.20","article-title":"Modular construction of cut-free sequent calculi for paraconsistent logics","volume-title":"2012 27th Annual IEEE Symposium on Logic in Computer Science (LICS)","author":"Avron","year":"2012"},{"key":"2019091313044445500_ref5","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-54458-7_18","article-title":"Classical system of Martin-L\u00f6f\u2019s inductive definitions is not equivalent to cyclic proof system","volume-title":"Proceedings of the 20$^th$ International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, Uppsala, Sweden, April 22\u201329, 2017","author":"Berardi","year":"2017"},{"key":"2019091313044445500_ref6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/LICS.2017.8005114","article-title":"Equivalence of inductive definitions and cyclic proofs under arithmetic","volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20\u201323, 2017","author":"Berardi","year":"2017"},{"key":"2019091313044445500_ref7","volume-title":"The Classical Decision Problem","author":"B\u00f6rger","year":"2001"},{"key":"2019091313044445500_ref8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-74061-2_6","article-title":"Formalised inductive reasoning in the logic of bunched implications","volume-title":"Proceedings of Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22\u201324, 2007","author":"Brotherston","year":"2007"},{"key":"2019091313044445500_ref9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328438.1328453","article-title":"Cyclic proofs of program termination in separation logic","volume-title":"Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008","author":"Brotherston","year":"2008"},{"key":"2019091313044445500_ref10","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","article-title":"Sequent calculi for induction and infinite descent","volume":"21","author":"Brotherston","year":"2010","journal-title":"Journal of Logic and Computation"},{"key":"2019091313044445500_ref11","first-page":"59","article-title":"On sequents and tableaux for many-valued logics","volume":"8","author":"Carnielli","year":"1991","journal-title":"Journal of Non-Classical Logic"},{"key":"2019091313044445500_ref12","volume-title":"Symbolic logic and mechanical theorem proving","author":"Chang","year":"2014"},{"key":"2019091313044445500_ref13","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-1-4684-3384-5_11","article-title":"Negation as failure","volume-title":"Logic and Data Bases","author":"Clark","year":"1978"},{"key":"2019091313044445500_ref14","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-319-66902-1_15","article-title":"Completeness for ancestral logic via a computationally-meaningful semantics","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Cohen","year":"2017"},{"key":"2019091313044445500_ref15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11229-015-0784-3","article-title":"The middle ground-ancestral logic","author":"Cohen","year":"2015","journal-title":"Synthese"},{"key":"2019091313044445500_ref16","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.4230\/LIPIcs.CSL.2018.16","article-title":"Uniform inductive reasoning in transitive closure logic via infinite descent","volume-title":"Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4\u20137, 2018, Birmingham, UK","author":"Cohen","year":"2018"},{"key":"2019091313044445500_ref17","first-page":"107","article-title":"Reasoning inside the box: deduction in herbrand logics","volume-title":"GCAI 2017. 3rd Global Conference on Artificial Intelligence","author":"Cohen","year":"2017"},{"key":"2019091313044445500_ref18","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-66902-1_16","article-title":"A cut-free cyclic proof system for Kleene algebra","volume-title":"Proceedings of the 26th International Conference Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX, Bras\u00edlia, Brazil, September 25\u201328, 2017","author":"Das","year":"2017"},{"key":"2019091313044445500_ref19","first-page":"243","article-title":"Rewrite systems","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)","author":"Dershowitz","year":"1990"},{"key":"2019091313044445500_ref20","first-page":"1","article-title":"Lectures on proof theory","volume-title":"Proceedings of the Summer School in Logic","author":"Feferman","year":"1968"},{"key":"2019091313044445500_ref21","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/BFb0079423","article-title":"First-order logic and its extensions","volume-title":"$\\models $ISILC Logic Conference","author":"Flum","year":"1975"},{"key":"2019091313044445500_ref22","volume-title":"Logic for computer science: foundations of automatic theorem proving.","author":"Gallier","year":"2015"},{"key":"2019091313044445500_ref23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01798-8","article-title":"Synthesis Lectures on Computer Science","volume-title":"Introduction to Logic","author":"Genesereth","year":"2012"},{"key":"2019091313044445500_ref24","first-page":"3","article-title":"The Herbrand manifesto\u2014thinking inside the box","volume-title":"Proceedings of the 9th International Symposium of RuleML","author":"Genesereth","year":"2015"},{"key":"2019091313044445500_ref25","article-title":"Investigations into logical deduction, 1934","volume-title":"An English translation appears in \u2018The Collected Works of Gerhard Gentzen\u2019","author":"Gentzen","year":"1969"},{"key":"2019091313044445500_ref26","article-title":"Herbrand logic","volume-title":"Technical Report","author":"Hinrichs","year":"2006"},{"key":"2019091313044445500_ref27","article-title":"The definition of E! in free logic","author":"Lambert","year":"1960","journal-title":"Abstracts: The International Congress for Logic, Methodology and Philosophy of Science"},{"key":"2019091313044445500_ref28","volume-title":"Foundations of Logic Programming","author":"Lloyd","year":"2012"},{"key":"2019091313044445500_ref29","volume-title":"Set theory, logic and their limitations","author":"Machover","year":"1996"},{"key":"2019091313044445500_ref30","volume-title":"Proof Theory for Fuzzy Logics","author":"Metcalfe","year":"2008"},{"key":"2019091313044445500_ref31","volume-title":"Gentzen calculi for modal propositional logic","author":"Poggiolesi","year":"2010"},{"key":"2019091313044445500_ref32","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1002\/malq.200810013","article-title":"Interpolation via translations","volume":"55","author":"Rasga","year":"2009","journal-title":"Mathematical Logic Quarterly"},{"key":"2019091313044445500_ref33","first-page":"729","article-title":"An essentially undecidable axiom system","volume-title":"Proceedings of the International Congress of Mathematics","author":"Robinson","year":"1950"},{"key":"2019091313044445500_ref34","volume-title":"Handbook of Automated Reasoning","author":"Robinson","year":"2001"},{"key":"2019091313044445500_ref35","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/3018610.3018623","article-title":"Automatic cyclic termination proofs for recursive procedures in separation logic","volume-title":"Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16\u201317, 2017","author":"Rowe","year":"2017"},{"key":"2019091313044445500_ref36","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-58025-5_65","article-title":"Definitional reflection and the completion","volume-title":"Extensions of Logic Programming: 4th International Workshop, ELP \u201893 St Andrews, U.K., March 29\u2013April 1, 1993 Proceedings","author":"Schroeder-Heister","year":"1994"},{"key":"2019091313044445500_ref37","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF01342849","article-title":"Beweistheoretische erfassung der unendlichen induktion in der zahlentheorie","volume":"122","author":"Sch\u00fctte","year":"1950","journal-title":"Mathematische Annalen"},{"key":"2019091313044445500_ref38","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1111\/j.1755-2567.1977.tb00778.x","article-title":"A completeness proof for an infinitary tense-logic","volume":"43","author":"Sundholm","year":"1977","journal-title":"Theoria"},{"key":"2019091313044445500_ref39","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-63046-5_30","article-title":"Automatically verifying temporal properties of pointer programs with cyclic proof","volume-title":"Proceedings of the 26th International Conference on Automated Deduction, CADE 26, Gothenburg, Sweden, August 6\u201311, 2017","author":"Tellez","year":"2017"},{"key":"2019091313044445500_ref40","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-94-010-0387-2_2","article-title":"Sequent systems for modal logics","volume-title":"Handbook of Philosophical Logic, 2nd edn.","author":"Wansing","year":"2002"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/advance-article-pdf\/doi\/10.1093\/logcom\/exz011\/28760686\/exz011.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/5\/693\/30010802\/exz011.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T19:59:32Z","timestamp":1694807972000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/5\/693\/5492446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,3]]},"references-count":40,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2019,6,3]]},"published-print":{"date-parts":[[2019,9,12]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz011","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2019,9]]},"published":{"date-parts":[[2019,6,3]]}}}