{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T20:41:01Z","timestamp":1649191261114},"reference-count":43,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2020,12,16]],"date-time":"2020-12-16T00:00:00Z","timestamp":1608076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"Google Summer of Code 2014 program"},{"name":"Google Summer of Code 2016 program"},{"name":"\u00d6sterreichischen Akademie der Wissenschaft (APART) an der TU Wien"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,12,22]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction\u2014CADE-23\u201423rd International Conference on Automated Deduction, Wroclaw, Poland, July 31\u2013August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.<\/jats:p>","DOI":"10.1093\/logcom\/exaa065","type":"journal-article","created":{"date-parts":[[2020,11,20]],"date-time":"2020-11-20T04:48:43Z","timestamp":1605847723000},"page":"1903-1932","source":"Crossref","is-referenced-by-count":0,"title":["Lifting propositional proof compression algorithms to first-order logic"],"prefix":"10.1093","volume":"31","author":[{"given":"Jan","family":"Gorzny","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Waterloo, Waterloo N2L 3G1, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ezequiel","family":"Postan","sequence":"additional","affiliation":[{"name":"Universidad Nacional de Rosario, Av. Pellegrini 250, S2000BTP Rosario, Santa Fe, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[{"name":"Faculty of Informatics, Vienna University of Technology, Vienna 1040, Austria and College of Engineering and Computer Science, Australian National University, Canberra ACT 0200, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,12,16]]},"reference":[{"key":"2021121717370444500_ref1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.05.025","article-title":"Compressing propositional refutations","volume":"185","author":"Amjad","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2021121717370444500_ref2","first-page":"114","article-title":"Linear-time reductions of resolution proofs","volume-title":"Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27\u201330, 2008","author":"Bar-Ilan","year":"2008"},{"key":"2021121717370444500_ref3","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-010-0167-5","article-title":"Reducing the size of resolution proofs in linear time","volume":"13","author":"Bar-Ilan","year":"2011","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2021121717370444500_ref4","first-page":"367","article-title":"Beagle\u2014a hierarchic superposition theorem prover","author":"Baumgartner","year":"2015"},{"key":"2021121717370444500_ref5","first-page":"24","article-title":"Automated reasoning for explainable artificial intelligence","volume-title":"ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017","author":"Bonacina","year":"2017"},{"key":"2021121717370444500_ref6","first-page":"59","article-title":"Compression of propositional resolution proofs by lowering subproofs","author":"Boudou","year":"2013"},{"key":"2021121717370444500_ref7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning\u201416th International Conference, LPAR-16, Dakar, Senegal, April 25\u2013May 1, 2010, Revised Selected Papers","author":"Clarke","year":"2010"},{"key":"2021121717370444500_ref8","first-page":"306","article-title":"Two techniques for minimizing resolution proofs","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11\u201314, 2010","author":"Cotton","year":"2010"},{"key":"2021121717370444500_ref9","volume-title":"Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond","author":"Cruanes","year":"2015"},{"key":"2021121717370444500_ref10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-21401-6","volume-title":"Automated Deduction\u2014CADE-25\u201425th International Conference on Automated Deduction, Berlin, Germany, August 1\u20137, 2015","author":"Felty","year":"2015"},{"key":"2021121717370444500_ref11","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-642-22438-6_19","article-title":"Compression of propositional resolution proofs via partial regularization","volume-title":"Automated Deduction\u2014CADE-23\u201423rd International Conference on Automated Deduction, Wroclaw, Poland, July 31\u2013August 5, 2011","author":"Fontaine","year":"2011"},{"key":"2021121717370444500_ref12","article-title":"Exploring and exploiting algebraic and graphical properties of resolution","volume-title":"8th International Workshop on SAT Modulo Theories Workshop (SMT)","author":"Fontaine","year":"2010"},{"key":"2021121717370444500_ref13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-40537-2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods\u201422th International Conference, TABLEAUX 2013, Nancy, France, September 16\u201319, 2013","author":"Galmiche","year":"2013"},{"key":"2021121717370444500_ref14","first-page":"356","article-title":"Towards the compression of first-order resolution proofs by lowering unit clauses","author":"Gorzny","year":"2015"},{"key":"2021121717370444500_ref15","first-page":"34","article-title":"Partial regularization of first-order resolution proofs","volume-title":"6th Global Conference on Artificial Intelligence, GCAI 2020, Hangzhou, China, April 6\u20139, 2020","author":"Gorzny","year":"2020"},{"key":"2021121717370444500_ref16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","article-title":"Algorithmic introduction of quantified cuts","volume":"549","author":"Hetzl","year":"2014","journal-title":"Theoretical Computer Science"},{"key":"2021121717370444500_ref17","first-page":"462","article-title":"Herbrand sequent extraction","volume-title":"Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28\u2013August 1, 2008","author":"Hetzl","year":"2008"},{"key":"2021121717370444500_ref18","first-page":"157","article-title":"Understanding resolution proofs through Herbrand\u2019s theorem","author":"Hetzl","year":"2013"},{"key":"2021121717370444500_ref19","first-page":"21","article-title":"Clausal proof compression","volume-title":"IWIL@LPAR 2015, 11th International Workshop on the Implementation of Logics, Suva, Fiji, November 23, 2015","author":"Heule","year":"2015"},{"key":"2021121717370444500_ref20","first-page":"228","article-title":"Solving and verifying the boolean pythagorean triples problem via cube-and-conquer","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2016\u201419th International Conference, Bordeaux, France, July 5\u20138, 2016","author":"Marijn","year":"2016"},{"key":"2021121717370444500_ref21","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","article-title":"Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method","volume":"38","author":"Hsiang","year":"1991","journal-title":"Journal of the ACM"},{"key":"2021121717370444500_ref22","article-title":"Prover9 and Mace4","author":"McCune","year":"2005\u20132010"},{"key":"2021121717370444500_ref23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2018.07.007","article-title":"Explanation in artificial intelligence: insights from the social sciences","volume":"267","author":"Miller","year":"2019","journal-title":"Artificial Intelligence"},{"key":"2021121717370444500_ref24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","article-title":"Complexity and related enhancements for automated theorem-proving programs","volume":"2","author":"Overbeek","year":"1976","journal-title":"Computers and Mathematics with Applications"},{"key":"2021121717370444500_ref25","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0898-1221(75)90019-X","article-title":"An implementation of hyper-resolution","volume":"1","author":"Overbeek","year":"1975","journal-title":"Computers and Mathematics with Applications"},{"key":"2021121717370444500_ref26","first-page":"463","article-title":"Atomic cut introduction by resolution: proof structuring and compression","author":"Paleo","year":"2010"},{"key":"2021121717370444500_ref27","first-page":"18","article-title":"SPASS+t","volume-title":"ESCoR: Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings","author":"Prevosto","year":"2006"},{"key":"2021121717370444500_ref28","first-page":"3","article-title":"Importing SMT and connection proofs as expansion trees","volume-title":"Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2\u20133, 2015","author":"Reis","year":"2015"},{"key":"2021121717370444500_ref29","first-page":"91","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov","year":"2002","journal-title":"AI Communications"},{"key":"2021121717370444500_ref30","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"International Journal of Computing and Mathematics"},{"key":"2021121717370444500_ref31","first-page":"182","article-title":"An efficient and flexible approach to resolution proof reduction","volume-title":"Hardware and Software: Verification and Testing\u20146th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4\u20137, 2010. Revised Selected Papers","author":"Rollini","year":"2010"},{"key":"2021121717370444500_ref32","first-page":"735","article-title":"System description: E 1.8","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning\u201419th International Conference, LPAR-19, Stellenbosch, South Africa, December 14\u201319, 2013","author":"Schulz","year":"2013"},{"key":"2021121717370444500_ref33","article-title":"Proof generation for saturating first-order theorem provers","volume-title":"All about Proofs, Proofs for All","author":"Schulz","year":"2015"},{"key":"2021121717370444500_ref34","first-page":"20","article-title":"Corg: commonsense reasoning using a theorem prover and machine learning","volume-title":"Selected Student Contributions and Workshop Papers of LuxLogAI 2018","author":"Siebert","year":"2018"},{"key":"2021121717370444500_ref35","first-page":"547","article-title":"Compressing propositional proofs by common subproof extraction","volume-title":"Computer Aided Systems Theory\u2014EUROCAST 2007, 11th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 12\u201316, 2007, Revised Selected Papers","author":"Sinz","year":"2007"},{"key":"2021121717370444500_ref36","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"2021121717370444500_ref37","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":"The American Mathematical Monthly"},{"key":"2021121717370444500_ref38","doi-asserted-by":"crossref","first-page":"1967","DOI":"10.1007\/978-3-642-81955-1_28","article-title":"On the complexity of derivation in propositional calculus","volume-title":"Automation of Reasoning: Classical Papers in Computational Logic","author":"Tseitin","year":"1983"},{"key":"2021121717370444500_ref39","first-page":"447","article-title":"Automated proof compression by invention of new definitions","author":"Vyskocil","year":"2010"},{"key":"2021121717370444500_ref40","first-page":"12","article-title":"Ordered resolution","volume-title":"Towards an Encyclopaedia of Proof Systems","author":"Waldmann","year":"2017"},{"key":"2021121717370444500_ref41","doi-asserted-by":"crossref","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","article-title":"Combining superposition, sorts and splitting","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","author":"Weidenbach","year":"2001"},{"key":"2021121717370444500_ref42","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","article-title":"SPASS version 3.5","volume-title":"Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2\u20137, 2009","author":"Weidenbach","year":"2009"},{"key":"2021121717370444500_ref43","volume-title":"Herbrand Sequent Extraction","author":"Paleo","year":"2007"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/8\/1903\/41809048\/exaa065.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/8\/1903\/41809048\/exaa065.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T19:07:53Z","timestamp":1639768073000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/8\/1903\/6038918"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,16]]},"references-count":43,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2020,12,16]]},"published-print":{"date-parts":[[2021,12,22]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa065","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2021,12]]},"published":{"date-parts":[[2020,12,16]]}}}