{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T11:43:06Z","timestamp":1710502986660},"reference-count":40,"publisher":"Oxford University Press (OUP)","issue":"7","license":[{"start":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:00:00Z","timestamp":1620000000000},"content-version":"vor","delay-in-days":0,"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":[[2022,7,15]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>$\\{log\\}$ (\u2018setlog\u2019) is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FS&amp;RA). As such, it can be used as an automated theorem prover for this theory. $\\{log\\}$ is able to automatically prove a number of FS&amp;RA theorems, but not all of them. Nevertheless, we have observed that many theorems that $\\{log\\}$ cannot automatically prove can be divided into a few subgoals automatically dischargeable by $\\{log\\}$. The purpose of this work is to present a prototype interactive theorem prover (ITP), called $\\{log\\}$-ITP, providing evidence that a proper integration of $\\{log\\}$ into world-class ITP\u2019s can deliver a great deal of proof automation concerning FS&amp;RA. An empirical evaluation based on 210 theorems from the TPTP and Coq\u2019s SSReflect libraries shows a noticeable reduction in the size and complexity of the proofs with respect to Coq.<\/jats:p>","DOI":"10.1093\/comjnl\/bxab030","type":"journal-article","created":{"date-parts":[[2021,3,17]],"date-time":"2021-03-17T20:10:08Z","timestamp":1616011808000},"page":"1891-1903","source":"Crossref","is-referenced-by-count":1,"title":["Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra"],"prefix":"10.1093","volume":"65","author":[{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[{"name":"Universidad Nacional de Rosario and CIFASIS , Pellegrini 250 - (2000) Rosario, Argentina"}]},{"given":"Ricardo D","family":"Katz","sequence":"additional","affiliation":[{"name":"CIFASIS-CONICET , Bv. 27 de febrero 210 bis - (2000) Rosario, Argentina"}]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Parma , Parco Area delle Scienze, 53\/A - 43100 PARMA, Italy"}]}],"member":"286","published-online":{"date-parts":[[2021,5,3]]},"reference":[{"key":"2022071813385581700_ref1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/B978-0-444-51624-4.50004-6","article-title":"History of interactive theorem proving","volume-title":"Computational Logic","author":"Harrison","year":"2014"},{"key":"2022071813385581700_ref2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions Texts in Theoretical Computer Science","author":"Bertot","year":"2004"},{"key":"2022071813385581700_ref3","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"2022071813385581700_ref4","first-page":"265","article-title":"HOL light: A tutorial introduction","volume-title":"Formal Methods in Computer-Aided Design, First International Conference, FMCAD \u201896, Palo Alto, California, USA, November 6\u20138, 1996, Proceedings","author":"Harrison","year":"1996"},{"key":"2022071813385581700_ref5","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","article-title":"Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T)","volume":"53","author":"Nieuwenhuis","year":"2006","journal-title":"J. ACM"},{"key":"2022071813385581700_ref6","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","article-title":"Hammer for coq: Automation for dependent type theory","volume":"61","author":"Czajka","year":"2018","journal-title":"J. Autom. Reasoning"},{"key":"2022071813385581700_ref7","first-page":"1","article-title":"Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers","volume-title":"The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011","author":"Paulson","year":"2010"},{"key":"2022071813385581700_ref8","first-page":"126","article-title":"Smtcoq: A plug-in for integrating SMT solvers into Coq","volume-title":"Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24\u201328, 2017, Proceedings, Part II","author":"Ekici","year":"2017"},{"key":"2022071813385581700_ref9","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","article-title":"Extending Sledgehammer with SMT solvers","volume":"51","author":"Blanchette","year":"2013","journal-title":"J. Autom. Reasoning"},{"key":"2022071813385581700_ref10","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","article-title":"Solving quantifier-free first-order constraints over finite sets and binary relations","volume":"64","author":"Cristi\u00e1","year":"2020","journal-title":"J. Autom. Reasoning"},{"key":"2022071813385581700_ref11","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson","year":"2006"},{"key":"2022071813385581700_ref12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"2022071813385581700_ref13","volume-title":"The Z Notation: A Reference Manual","author":"Spivey","year":"1992"},{"key":"2022071813385581700_ref14","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","article-title":"The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0","volume":"43","author":"Sutcliffe","year":"2009","journal-title":"J. Autom. Reasoning"},{"key":"2022071813385581700_ref15","first-page":"333","article-title":"A set solver for finite set relation algebra","volume-title":"Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29\u2013November 1, 2018, Proceedings","author":"Cristi\u00e1","year":"2018"},{"key":"2022071813385581700_ref16","doi-asserted-by":"crossref","DOI":"10.1090\/memo\/0604","volume-title":"Decision Problems for Equational Theories of Relation Algebras","author":"Andr\u00e9ka","year":"1997"},{"key":"2022071813385581700_ref17","first-page":"238","article-title":"Discharging proof obligations from Atelier B using multiple automated provers","volume-title":"ABZ, Lecture Notes in Computer Science","author":"Mentr\u00e9","year":"2012"},{"key":"2022071813385581700_ref18","article-title":"Why3: Shepherd your herd of provers","volume-title":"Boogie 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot","year":"2011"},{"key":"2022071813385581700_ref19","article-title":"Quickchick: Property-Based Testing for Coq","author":"D\u00e9n\u00e8s","year":"2014","journal-title":"The Coq Workshop"},{"key":"2022071813385581700_ref20","first-page":"111","article-title":"E - a brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Commun."},{"key":"2022071813385581700_ref21","first-page":"91","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov","year":"2002","journal-title":"AI Commun."},{"key":"2022071813385581700_ref22","first-page":"1","article-title":"Encoding monomorphic and polymorphic types","volume":"12","author":"Blanchette","year":"2016","journal-title":"Logical Methods in Computer Science"},{"key":"2022071813385581700_ref23","first-page":"42","article-title":"Automated deduction in the B set theory using typed proof search and deduction modulo","volume-title":"20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24\u201328, 2015","author":"Bury","year":"2015"},{"key":"2022071813385581700_ref24","first-page":"409","article-title":"An automation-friendly set theory for the B method","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5\u20138, 2018, Proceedings","author":"Bury","year":"2018"},{"key":"2022071813385581700_ref25","volume-title":"Alt-Ergo","author":"Conchon"},{"key":"2022071813385581700_ref26","volume-title":"ArchSat","author":"Bury"},{"key":"2022071813385581700_ref27","volume-title":"Zipperposition","author":"Cruanes"},{"key":"2022071813385581700_ref28","first-page":"179","article-title":"A decision procedure for sets, binary relations and partial functions","volume-title":"Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Proceedings, Part I","author":"Cristi\u00e1","year":"2016"},{"key":"2022071813385581700_ref29","author":"Rossi","year":"2008"},{"key":"2022071813385581700_ref30","article-title":"Using a set constraint solver for program verification","volume-title":"Proceedings 4th Workshop on Horn Clauses for Verification and Synthesis, HCVS at CADE 2017, Gothenburg, Sweden, 7th August 2017","author":"Cristi\u00e1","year":"2017"},{"key":"2022071813385581700_ref31","first-page":"229","article-title":"log as a test case generator for the Test Template Framework","volume-title":"SEFM, Lecture Notes in Computer Science","author":"Cristi\u00e1","year":"2013"},{"key":"2022071813385581700_ref32","first-page":"4","article-title":"Rapid prototyping and animation of Z specifications using log","volume-title":"1st International Workshop about Sets and Tools (SETS 2014)","author":"Cristi\u00e1","year":"2014"},{"key":"2022071813385581700_ref33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-6510-2_3","article-title":"Heterogeneous Relation Algebra","volume-title":"Relational Methods in Computer Science","author":"Schmidt","year":"1997"},{"key":"2022071813385581700_ref34","article-title":"Automated proof of Bell\u2013LaPadula security properties","author":"Cristi\u00e1","year":"2020","journal-title":"J. Autom. Reasoning"},{"key":"2022071813385581700_ref35","article-title":"An automatically verified prototype of the Tokeneer ID station specification","author":"Cristi\u00e1","year":"2020","journal-title":"CoRR"},{"key":"2022071813385581700_ref36","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1145\/365151.365169","article-title":"Sets and constraint logic programming","volume":"22","author":"Dovier","year":"2000","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2022071813385581700_ref37","volume-title":"Rewrite rules for a solver for sets, binary relations and partial functions","author":"Cristi\u00e1","year":"2019"},{"key":"2022071813385581700_ref38","volume-title":"log -ITP source code and experimental data","author":"Cristi\u00e1","year":"2019"},{"key":"2022071813385581700_ref39","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"J. Formalized Reasoning"},{"key":"2022071813385581700_ref40","first-page":"32","article-title":"Towards Coq formalisation of log set constraints resolution","volume-title":"Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, SETS@ABZ 2018, Southamptom, UK, June 5, 2018","author":"Dubois","year":"2018"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/65\/7\/1891\/44921662\/bxab030.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/65\/7\/1891\/44921662\/bxab030.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T13:40:55Z","timestamp":1658151655000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/65\/7\/1891\/6262250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,3]]},"references-count":40,"journal-issue":{"issue":"7","published-online":{"date-parts":[[2021,5,3]]},"published-print":{"date-parts":[[2022,7,15]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxab030","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,7,15]]},"published":{"date-parts":[[2021,5,3]]}}}