{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T03:26:43Z","timestamp":1762918003629,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T00:00:00Z","timestamp":1554681600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006668","name":"Fondo para la Investigaci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["PICT-2014-2200"],"award-info":[{"award-number":["PICT-2014-2200"]}],"id":[{"id":"10.13039\/501100006668","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1007\/s10817-019-09520-4","type":"journal-article","created":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T04:14:22Z","timestamp":1554696862000},"page":"295-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations"],"prefix":"10.1007","volume":"64","author":[{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,8]]},"reference":[{"key":"9520_CR1","volume-title":"Decision Problems for Equational Theories of Relation Algebras","author":"H Andr\u00e9ka","year":"1997","unstructured":"Andr\u00e9ka, H., Givant, S.R., N\u00e9meti, I.: Decision Problems for Equational Theories of Relation Algebras, vol. 604. American Mathematical Society, Providence (1997)"},{"issue":"1","key":"9520_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s00165-016-0369-z","volume":"29","author":"EJG Arias","year":"2017","unstructured":"Arias, E.J.G., Lipton, J., Mari\u00f1o, J.: Constraint logic programming with a relational machine. For. Asp. Comput. 29(1), 97\u2013124 (2017). \nhttps:\/\/doi.org\/10.1007\/s00165-016-0369-z","journal-title":"For. Asp. Comput."},{"key":"9520_CR3","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"Alasdair Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving\u20144th International Conference, ITP 2013, Rennes, France, July 22\u201326, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7998, pp. 197\u2013212. Springer, Berlin (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_16"},{"issue":"1","key":"9520_CR4","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10601-006-9012-6","volume":"12","author":"F Azevedo","year":"2007","unstructured":"Azevedo, F.: Cardinal: a finite sets constraint solver. Constraints 12(1), 93\u2013129 (2007). \nhttps:\/\/doi.org\/10.1007\/s10601-006-9012-6","journal-title":"Constraints"},{"key":"9520_CR5","unstructured":"Berghammer, R.: Relview. \nhttp:\/\/www.informatik.uni-kiel.de\/~progsys\/relview\/"},{"issue":"3","key":"9520_CR6","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S1571-0661(04)80931-9","volume":"44","author":"R Berghammer","year":"2001","unstructured":"Berghammer, R., Hoffmann, T., Leoniuk, B., Milanese, U.: Prototyping and programming with relations. Electr. Notes Theor. Comput. Sci. 44(3), 27\u201350 (2001). \nhttps:\/\/doi.org\/10.1016\/S1571-0661(04)80931-9","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9520_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-06251-8_11","volume-title":"Relational and Algebraic Methods in Computer Science","author":"Rudolf Berghammer","year":"2014","unstructured":"Berghammer, R., H\u00f6fner, P., Stucke, I.: Automated verification of relational while-programs. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) Relational and Algebraic Methods in Computer Science\u201414th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28\u2013May 1, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8428, pp. 173\u2013190. Springer, Berlin (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-06251-8_11"},{"issue":"10","key":"9520_CR8","doi-asserted-by":"publisher","first-page":"915","DOI":"10.1002\/spe.597","volume":"34","author":"E Bernard","year":"2004","unstructured":"Bernard, E., Legeard, B., Luck, X., Peureux, F.: Generation of test sequences from formal specifications: GSM 11-11 standard case study. Int. J. Softw. Pract. Exp. 34(10), 915\u2013948 (2004)","journal-title":"Int. J. Softw. Pract. Exp."},{"key":"9520_CR9","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: 1st International Workshop on Intermediate Verification Languages. Wroc\u0142aw, Poland (August 2011). \nhttp:\/\/proval.lri.fr\/submissions\/boogie11.pdf"},{"key":"9520_CR10","unstructured":"Broome, P., Lipton, J.: Combinatory logic programming: computing in relation calculi. In: Bruynooghe, M. (ed.) Logic Programming, Proceedings of the 1994 International Symposium, Ithaca, New York, USA, November 13\u201317, 1994, pp. 269\u2013285. MIT Press, Cambridge (1994)"},{"key":"9520_CR11","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2014.03.021","volume":"560","author":"D Cantone","year":"2014","unstructured":"Cantone, D., Longo, C.: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions. Theor. Comput. Sci. 560, 307\u2013325 (2014). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2014.03.021","journal-title":"Theor. Comput. Sci."},{"key":"9520_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing\u2014from Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science","author":"D Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing\u2014from Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, Berlin (2001). \nhttps:\/\/doi.org\/10.1007\/978-1-4757-3452-2"},{"issue":"2","key":"9520_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/BF00243808","volume":"7","author":"D Cantone","year":"1991","unstructured":"Cantone, D., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory: XI. Multilevel syllogistic extended by some elementary map constructs. J. Autom. Reason. 7(2), 231\u2013256 (1991). \nhttps:\/\/doi.org\/10.1007\/BF00243808","journal-title":"J. Autom. Reason."},{"key":"9520_CR14","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model building. In: CADE-19 Workshop: Model Computation\u2014Principles, Algorithms, Applications, pp. 11\u201327 (2003)"},{"key":"9520_CR15","unstructured":"Clearsy: Aterlier B home page. \nhttp:\/\/www.atelierb.eu\/"},{"key":"9520_CR16","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-33951-1_18","volume-title":"Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo","author":"S Conchon","year":"2016","unstructured":"Conchon, S., Iguernlala, M.: Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, pp. 243\u2013253. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33951-1_18"},{"key":"9520_CR17","unstructured":"Coq Development Team: The Coq proof assistant reference manual, version 8.8.1. LogiCal Project, Palaiseau (2018)"},{"key":"9520_CR18","unstructured":"Cristi\u00e1, M., Rossi, G.: Rewrite rules for a solver for sets, binary relations and partial functions. \nhttp:\/\/people.dmi.unipr.it\/gianfranco.rossi\/SETLOG\/calculus.pdf"},{"key":"9520_CR19","unstructured":"Cristi\u00e1, M., Rossi, G.: Rapid prototyping and animation of Z specifications using \n$$\\{\\log \\}$$\n\n\n\n\n{\nlog\n}\n\n\n\n\n. In: 1st International Workshop about Sets and Tools (SETS 2014), pp. 4\u201318 (2014), Informal Proceedings. \nhttp:\/\/sets2014.cnam.fr\/papers\/sets2014.pdf"},{"key":"9520_CR20","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-41528-4_10","volume-title":"Computer Aided Verification","author":"Maximiliano Cristi\u00e1","year":"2016","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification\u201428th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9779, pp. 179\u2013198. Springer, Berlin (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41528-4_10"},{"key":"9520_CR21","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-63046-5_12","volume-title":"Automated Deduction \u2013 CADE 26","author":"Maximiliano Cristi\u00e1","year":"2017","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de\u00a0Moura [28], pp. 185\u2013201. \nhttps:\/\/doi.org\/10.1007\/978-3-319-63046-5_12"},{"key":"9520_CR22","unstructured":"Cristi\u00e1, M., Rossi, G.: Detailed proofs of \n$${\\cal{L}}_{{\\cal{BR}}}$$\n\n\n\n\nL\nBR\n\n\n\n\n properties for the paper: \u201csolving quantifier-free first-order constraints over finite sets and binary relations\u201d (2018). \nhttps:\/\/www.dropbox.com\/s\/jlisk0vngeb42c3\/proofs.pdf?dl=0"},{"key":"9520_CR23","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.: Using a set constraint solver for program verification. In: Proceedings 4th Workshop on Horn Clauses for Verification and Synthesis, HCVS@CADE 2017, Gothenburg, Sweden, 7th August 2017 (2017). \nhttp:\/\/software.imdea.org\/Conferences\/hcvs17\/"},{"key":"9520_CR24","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-40561-7_16","volume-title":"Software Engineering and Formal Methods","author":"Maximiliano Cristi\u00e1","year":"2013","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229\u2013243. Springer, Berlin (2013)"},{"issue":"4\u20135","key":"9520_CR25","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1017\/S1471068415000290","volume":"15","author":"M Cristi\u00e1","year":"2015","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: Adding partial functions to constraint logic programming with sets. TPLP 15(4\u20135), 651\u2013665 (2015). \nhttps:\/\/doi.org\/10.1017\/S1471068415000290","journal-title":"TPLP"},{"key":"9520_CR26","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in rodin. Sci. Comput. Program. 94, 130\u2013143 (2014). \nhttps:\/\/doi.org\/10.1016\/j.scico.2014.04.012","journal-title":"Sci. Comput. Program."},{"key":"9520_CR27","unstructured":"Deville, Y., Dooms, G., Zampelli, S., Dupont, P.: CP(graph+map) for approximate graph matching. In: 1st International Workshop on Constraint Programming Beyond Finite Integer Domains, pp. 31\u201347 (2005)"},{"key":"9520_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5","volume-title":"Automated Deduction \u2013 CADE 26","year":"2017","unstructured":"de\u00a0Moura, L. (ed.): Automated Deduction\u2014CADE 26\u201326th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10395. Springer, Berlin (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63046-5"},{"key":"9520_CR29","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15\u201318 November 2009, Austin, Texas, USA, pp. 45\u201352. IEEE, New York (2009). \nhttps:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"1","key":"9520_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0743-1066(95)00147-6","volume":"28","author":"A Dovier","year":"1996","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. Log. Program. 28(1), 1\u201344 (1996). \nhttps:\/\/doi.org\/10.1016\/0743-1066(95)00147-6","journal-title":"J. Log. Program."},{"issue":"5","key":"9520_CR31","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9520_CR32","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645\u2013701 (2006). \nhttps:\/\/doi.org\/10.1017\/S1471068406002730","journal-title":"Theory Pract. Log. Program."},{"issue":"3","key":"9520_CR33","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF00137870","volume":"1","author":"C Gervet","year":"1997","unstructured":"Gervet, C.: Interval propagation to reason about sets: definition and implementation of a practical language. Constraints 1(3), 191\u2013244 (1997). \nhttps:\/\/doi.org\/10.1007\/BF00137870","journal-title":"Constraints"},{"issue":"4","key":"9520_CR34","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10817-006-9062-x","volume":"37","author":"S Givant","year":"2006","unstructured":"Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reasoning 37(4), 277\u2013322 (2006). \nhttps:\/\/doi.org\/10.1007\/s10817-006-9062-x","journal-title":"J. Autom. Reasoning"},{"key":"9520_CR35","unstructured":"Guttmann, W., Struth, G., Weber, T.: A repository for Tarski\u2013Kleene algebras. In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) Proceedings of the 5th Workshop on Automated Theory Engineering, Wroc\u0142aw, Poland, July 31, 2011. CEUR Workshop Proceedings, vol. 760, pp. 30\u201339. CEUR-WS.org (2011). \nhttp:\/\/ceur-ws.org\/Vol-760\/paper5.pdf"},{"key":"9520_CR36","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1613\/jair.1638","volume":"24","author":"P Hawkins","year":"2005","unstructured":"Hawkins, P., Lagoon, V., Stuckey, P.J.: Solving set constraint satisfaction problems using ROBDDs. J. Artif. Intell. Res. (JAIR) 24, 109\u2013156 (2005). \nhttps:\/\/doi.org\/10.1613\/jair.1638","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9520_CR37","unstructured":"Hinman, P.: Fundamentals of Mathematical Logic. CRC Press, Boca Raton (2018). \nhttps:\/\/books.google.it\/books?id=6UBZDwAAQBAJ"},{"key":"9520_CR38","doi-asserted-by":"publisher","unstructured":"H\u00f6fner, P., Struth, G.: On automating the calculus of relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 50\u201366. Springer, Berlin (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71070-7_5","DOI":"10.1007\/978-3-540-71070-7_5"},{"key":"9520_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44880-2_1","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"Daniel Jackson","year":"2003","unstructured":"Jackson, D.: Alloy: A logical modelling language. In: Bert, D., Bowen, J.P., King, S., Wald\u00e9n, M.A. (eds.) ZB 2003: Formal Specification and Development in Z and B, 3rd International Conference of B and Z Users, Turku, Finland, June 4\u20136, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2651, p.\u00a01. Springer, Berlin (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44880-2_1"},{"key":"9520_CR40","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)"},{"issue":"1","key":"9520_CR41","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlap.2007.10.008","volume":"76","author":"W Kahl","year":"2008","unstructured":"Kahl, W.: Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types. J. Log. Algebra Program. 76(1), 60\u201389 (2008). \nhttps:\/\/doi.org\/10.1016\/j.jlap.2007.10.008","journal-title":"J. Log. Algebra Program."},{"key":"9520_CR42","unstructured":"Kr\u00f6ning, D., R\u00fcmmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the SMT-Lib standard. In: Informal proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE 22 (2009)"},{"key":"9520_CR43","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"Michael Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Keijiro, A., Gnesi, S., Mandrioli, D. (eds.) FME. Lecture Notes in Computer Science, vol. 2805, pp. 855\u2013874. Springer, Berlin (2003)"},{"key":"9520_CR44","unstructured":"McCune, W.: Prover9 and mace4 (2005\u20132010). \nhttp:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"9520_CR45","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-63046-5_10","volume-title":"Automated Deduction \u2013 CADE 26","author":"Baoluo Meng","year":"2017","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de\u00a0Moura [28], pp. 148\u2013165. \nhttps:\/\/doi.org\/10.1007\/978-3-319-63046-5_10"},{"key":"9520_CR46","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"David Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.C., Asuka, M.: Discharging proof obligations from Atelier B using multiple automated provers. In: Derrick, J., Fitzgerald, J.A., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ. Lecture Notes in Computer Science, vol. 7316, pp. 238\u2013251. Springer, Berlin (2012)"},{"key":"9520_CR47","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002)"},{"key":"9520_CR48","unstructured":"Rossi, G.: \n$$\\{\\log \\}$$\n\n\n\n\n{\nlog\n}\n\n\n\n\n (2008). \nhttp:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html"},{"key":"9520_CR49","unstructured":"Saaltink, M.: The Z\/EVES mathematical toolkit version 2.2 for Z\/EVES version 1.5. Techical Report, ORA Canada (1997)"},{"key":"9520_CR50","first-page":"72","volume-title":"ZUM. Lecture Notes in Computer Science","author":"M Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM. Lecture Notes in Computer Science, vol. 1212, pp. 72\u201385. Springer, Berlin (1997)"},{"key":"9520_CR51","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-7091-6510-2_3","volume-title":"Heterogeneous Relation Algebra","author":"G Schmidt","year":"1997","unstructured":"Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous Relation Algebra, pp. 39\u201353. Springer, Vienna (1997). \nhttps:\/\/doi.org\/10.1007\/978-3-7091-6510-2_3"},{"issue":"4","key":"9520_CR52","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9520_CR53","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73\u201389 (1941). \nhttps:\/\/doi.org\/10.2307\/2268577","journal-title":"J. Symb. Log."},{"key":"9520_CR54","doi-asserted-by":"publisher","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24\u2013April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4424, pp. 632\u2013647. Springer, Berlin (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_49","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"9520_CR55","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-61511-3_96","volume-title":"Automated Deduction \u2014 Cade-13","author":"Jian Zhang","year":"1996","unstructured":"Zhang, J., Zhang, H.: System description: generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction\u2014CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30\u2013August 3, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1104, pp. 308\u2013312. Springer, Berlin (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-61511-3_96"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09520-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09520-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09520-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T23:10:44Z","timestamp":1586214644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09520-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,8]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["9520"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09520-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,4,8]]},"assertion":[{"value":"19 June 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}