{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:06Z","timestamp":1740123366807,"version":"3.37.3"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,4,5]],"date-time":"2021-04-05T00:00:00Z","timestamp":1617580800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,4,5]],"date-time":"2021-04-05T00:00:00Z","timestamp":1617580800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10817-021-09589-w","type":"journal-article","created":{"date-parts":[[2021,4,5]],"date-time":"2021-04-05T13:03:01Z","timestamp":1617627781000},"page":"809-890","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Automated Reasoning with Restricted Intensional Sets"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,4,5]]},"reference":[{"key":"9589_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"issue":"3","key":"9589_CR2","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0743-1066(90)90023-X","volume":"8","author":"R Barbuti","year":"1990","unstructured":"Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. J. Log. Program. 8(3), 201\u2013228 (1990). https:\/\/doi.org\/10.1016\/0743-1066(90)90023-X","journal-title":"J. Log. Program."},{"issue":"3&4","key":"9589_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0743-1066(91)90036-O","volume":"10","author":"C Beeri","year":"1991","unstructured":"Beeri, C., Naqvi, S.A., Shmueli, O., Tsur, S.: Set constructors in a logic database language. J. Log. Program. 10(3&4), 181\u2013232 (1991). https:\/\/doi.org\/10.1016\/0743-1066(91)90036-O","journal-title":"J. Log. Program."},{"key":"9589_CR4","unstructured":"Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical foundations. MTR 2547, The MITRE Corporation (1973)"},{"key":"9589_CR5","unstructured":"Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical model. ESD-TR 73-278, The MITRE Corporation (1973)"},{"key":"9589_CR6","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20\u201322, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7935, pp. 105\u2013125. Springer (2013). 1007\/978-3-642-38856-9\\_8"},{"key":"9589_CR7","unstructured":"Bruscoli, P., Dovier, A., Pontelli, E., Rossi, G.: Compiling intensional sets in CLP. In: Hentenryck, P.V. (ed.) Logic Programming, Proceedings of the Eleventh International Conference on Logic Programming, Santa Marherita Ligure, Italy, June 13\u201318, 1994. pp. 647\u2013661. MIT Press (1994)"},{"issue":"6","key":"9589_CR8","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/s10817-019-09533-z","volume":"64","author":"G Burel","year":"2020","unstructured":"Burel, G., Bury, G., Cauderlier, R., Delahaye, D., Halmagrand, P., Hermant, O.: First-order automated reasoning with theories: when deduction modulo theory meets practice. J. Autom. Reasoning 64(6), 1001\u20131050 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09533-z","journal-title":"J. Autom. Reasoning"},{"issue":"3\u20134","key":"9589_CR9","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1017\/S1471068418000169","volume":"18","author":"P Cabalar","year":"2018","unstructured":"Cabalar, P., Fandinno, J., del Cerro, L.F., Pearce, D.: Functional ASP with intensional sets: application to Gelfond-Zhang aggregates. Theory Pract. Log. Program. 18(3\u20134), 390\u2013405 (2018). https:\/\/doi.org\/10.1017\/S1471068418000169","journal-title":"Theory Pract. Log. Program."},{"key":"9589_CR10","volume-title":"Computable Set Theory","author":"D Cantone","year":"1989","unstructured":"Cantone, D., Ferro, A., Omodeo, E.: Computable Set Theory. Clarendon Press, USA (1989)"},{"key":"9589_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). https:\/\/doi.org\/10.1016\/j.tcs.2014.03.021","journal-title":"Theor. Comput. Sci."},{"key":"9589_CR12","doi-asserted-by":"crossref","unstructured":"Cantone, D., Zarba, C.G.: A tableau calculus for integrating first-order and elementary set theory reasoning. In: Dyckhoff, R. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1847, pp. 143\u2013159. Springer (2000). 1007\/10722086\\_14","DOI":"10.1007\/10722086_14"},{"key":"9589_CR13","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model building. In: CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications. pp. 11\u201327 (2003)"},{"key":"9589_CR14","unstructured":"Clearsy: Aterlier B home page, http:\/\/www.atelierb.eu\/"},{"key":"9589_CR15","doi-asserted-by":"crossref","unstructured":"Conchon, S., Iguernlala, M.: Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, pp. 243\u2013253. Springer, Cham (2016). 1007\/978-3-319-33951-1\\_18","DOI":"10.1007\/978-3-319-33951-1_18"},{"key":"9589_CR16","unstructured":"Cristi\u00e1, M., Fois, A., Rossi, G.: Declarative programming with intensional sets in java using jsetl. CoRR abs\/2002.11562 (2020), https:\/\/arxiv.org\/abs\/2002.11562"},{"key":"9589_CR17","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de\u00a0Moura, L. (ed.) Automated Deduction - CADE 26\u201326th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185\u2013201. Springer (2017), 1007\/978-3-319-63046-5\\_12","DOI":"10.1007\/978-3-319-63046-5_12"},{"key":"9589_CR18","unstructured":"Cristi\u00e1, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333\u2013349. Springer (2018). 1007\/978-3-030-02149-8\\_20"},{"key":"9589_CR19","unstructured":"Cristi\u00e1, M., Rossi, G.: Rewrite rules for a solver for sets, binary relations and partial functions (2019), http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/SETLOG\/calculus.pdf"},{"key":"9589_CR20","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated proof of Bell\u2013LaPadula security properties. J. Autom. Reasoning n\/a(n\/a) (jul 2020), https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09577-6","DOI":"10.1007\/s10817-020-09577-6"},{"key":"9589_CR21","unstructured":"Cristi\u00e1, M., Rossi, G.: An automatically verified prototype of the Tokeneer ID station specification. CoRR abs\/2009.00999 (2020), https:\/\/arxiv.org\/abs\/2009.00999"},{"issue":"2","key":"9589_CR22","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2020","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reasoning 64(2), 295\u2013330 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09520-4","journal-title":"J. Autom. Reasoning"},{"key":"9589_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 at CADE 2017, Gothenburg, Sweden, 7th August 2017. (2017), http:\/\/software.imdea.org\/Conferences\/hcvs17\/"},{"key":"9589_CR24","doi-asserted-by":"crossref","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 (2013)","DOI":"10.1007\/978-3-642-40561-7_16"},{"issue":"4\u20135","key":"9589_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). https:\/\/doi.org\/10.1017\/S1471068415000290","journal-title":"TPLP"},{"key":"9589_CR26","doi-asserted-by":"crossref","unstructured":"Dal Pal\u00fa, A., Dovier, A., Pontelli, E., Rossi, G.: Integrating finite domain constraints and CLP with sets. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming. pp. 219\u2013229. PPDP \u201903, ACM, New York (2003), http:\/\/doi.acm.org\/10.1145\/888251.888272","DOI":"10.1145\/888251.888272"},{"key":"9589_CR27","unstructured":"Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules for SMT proofs. In: Workshop on Proof eXchange for Theorem Proving (2011)"},{"key":"9589_CR28","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The bware project: Building a proof platform for the automated verification of B proof obligations. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, June 2\u20136, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8477, pp. 290\u2013293. Springer (2014). 1007\/978-3-662-43652-3\\_26"},{"issue":"1","key":"9589_CR29","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). https:\/\/doi.org\/10.1016\/0743-1066(95)00147-6","journal-title":"J. Log. Program."},{"issue":"5","key":"9589_CR30","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":"3","key":"9589_CR31","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BF03037598","volume":"19","author":"A Dovier","year":"2001","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Constructive negation and constraint logic programming with sets. New Gener. Comput. 19(3), 209\u2013256 (2001). https:\/\/doi.org\/10.1007\/BF03037598","journal-title":"New Gener. Comput."},{"key":"9589_CR32","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Intensional sets in CLP. In: Palamidessi, C. (ed.) Logic Programming, 19th International Conference, ICLP 2003, Mumbai, India, December 9\u201313, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2916, pp. 284\u2013299. Springer (2003). 1007\/978-3-540-24599-5\\_20"},{"issue":"6","key":"9589_CR33","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)","journal-title":"Theory Pract. Log Program"},{"key":"9589_CR34","unstructured":"Dragoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19\u201321, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8318, pp. 161\u2013181. Springer (2014). 1007\/978-3-642-54013-4\\_10"},{"issue":"4","key":"9589_CR35","doi-asserted-by":"publisher","first-page":"25:1","DOI":"10.1145\/1970398.1970401","volume":"12","author":"P Ferraris","year":"2011","unstructured":"Ferraris, P.: Logic programs with propositional connectives and aggregates. ACM Trans. Comput. Log. 12(4), 25:1\u201325:40 (2011). https:\/\/doi.org\/10.1145\/1970398.1970401","journal-title":"ACM Trans. Comput. Log."},{"key":"9589_CR36","doi-asserted-by":"crossref","unstructured":"Gao, C., Chen, T., Wu, Z.: Separation logic with linearly compositional inductive predicates and set data constraints. In: Catania, B., Kr\u00e1lovic, R., Nawrocki, J.R., Pighizzini, G. (eds.) SOFSEM 2019: Theory and Practice of Computer Science - 45th International Conference on Current Trends in Theory and Practice of Computer Science, Nov\u00fd Smokovec, Slovakia, January 27-30, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11376, pp. 206\u2013220. Springer (2019). 1007\/978-3-030-10801-4\\_17","DOI":"10.1007\/978-3-030-10801-4_17"},{"key":"9589_CR37","unstructured":"Ge, Y., de\u00a0Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 306\u2013320. Springer (2009). 1007\/978-3-642-02658-4\\_25"},{"issue":"4\u20135","key":"9589_CR38","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1017\/S1471068415000150","volume":"15","author":"M Gebser","year":"2015","unstructured":"Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., Schaub, T.: Abstract gringo. Theory Pract. Log Program 15(4\u20135), 449\u2013463 (2015). https:\/\/doi.org\/10.1017\/S1471068415000150","journal-title":"Theory Pract. Log Program"},{"key":"9589_CR39","volume-title":"The G\u00f6del Programming Language","author":"PM Hill","year":"1994","unstructured":"Hill, P.M., Lloyd, J.W.: The G\u00f6del Programming Language. MIT Press, Cambridge (1994)"},{"key":"9589_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)"},{"key":"9589_CR41","unstructured":"Lam, E.S.L., Cervesato, I.: Reasoning about set comprehensions. In: R\u00fcmmer, P., Wintersteiger, C.M. (eds.) Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, affiliated with the 26th International Conference on Computer Aided Verification (CAV 2014), the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, July 17\u201318, 2014. CEUR Workshop Proceedings, vol. 1163, pp. 27\u201337. CEUR-WS.org (2014), http:\/\/ceur-ws.org\/Vol-1163\/paper-05.pdf"},{"key":"9589_CR42","doi-asserted-by":"crossref","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 (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"issue":"2","key":"9589_CR43","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-015-0391-0","volume":"19","author":"A Mammar","year":"2017","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in event-b. Int. J. Softw. Tools Technol. Transf. 19(2), 167\u2013186 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0391-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9589_CR44","doi-asserted-by":"crossref","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 (2012)","DOI":"10.1007\/978-3-642-30885-7_17"},{"key":"9589_CR45","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.004","volume":"158","author":"S Merz","year":"2018","unstructured":"Merz, S., Vanzetto, H.: Encoding tla$${}^{\\text{+ }}$$ into unsorted and many-sorted first-order logic. Sci. Comput. Program. 158, 3\u201320 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.09.004","journal-title":"Sci. Comput. Program."},{"key":"9589_CR46","unstructured":"Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P., Schwichtenberg, H. (eds.) Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1862, pp. 411\u2013426. Springer (2000). 1007\/3-540-44622-2\\_28"},{"key":"9589_CR47","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: Minizinc: Towards a standard CP modelling language. In: Bessiere, C. (ed.) Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23\u201327, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4741, pp. 529\u2013543. Springer (2007). 1007\/978-3-540-74970-7\\_38"},{"key":"9589_CR48","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 640\u2013655. Springer (2013). 1007\/978-3-642-39799-8\\_42"},{"key":"9589_CR49","unstructured":"Rossi, G.: $$\\{log\\}$$. http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html (2008), http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html"},{"issue":"2","key":"9589_CR50","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1002\/spe.749","volume":"37","author":"G Rossi","year":"2007","unstructured":"Rossi, G., Panegai, E., Poleo, E.: Jsetl: a java library for supporting declarative programming in java. Softw. Pract. Exp. 37(2), 115\u2013149 (2007)","journal-title":"Softw. Pract. Exp."},{"key":"9589_CR51","doi-asserted-by":"crossref","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 (1997)","DOI":"10.1007\/BFb0027284"},{"key":"9589_CR52","unstructured":"Schneider, S.: The B-method: An Introduction. Cornerstones of computing, Palgrave (2001), http:\/\/books.google.com.ar\/books?id=Krs0OQAACAAJ"},{"key":"9589_CR53","doi-asserted-by":"publisher","unstructured":"Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets - An Introduction to SETL. Texts and Monographs in Computer Science, Springer (1986), https:\/\/doi.org\/10.1007\/978-1-4613-9575-1","DOI":"10.1007\/978-1-4613-9575-1"},{"issue":"3","key":"9589_CR54","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1017\/S1471068406002936","volume":"7","author":"TC Son","year":"2007","unstructured":"Son, T.C., Pontelli, E.: A constructive semantic characterization of aggregates in answer set programming. Theory Pract. Log. Program. 7(3), 355\u2013375 (2007). https:\/\/doi.org\/10.1017\/S1471068406002936","journal-title":"Theory Pract. Log. Program."},{"key":"9589_CR55","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)"},{"issue":"4","key":"9589_CR56","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."},{"key":"9589_CR57","unstructured":"Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22\u201327, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5330, pp. 305\u2013317. Springer (2008). 1007\/978-3-540-89439-1\\_22"},{"key":"9589_CR58","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16\u201318, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5749, pp. 366\u2013382. Springer (2009). 1007\/978-3-642-04222-5\\_23"},{"key":"9589_CR59","volume-title":"Using Z: specification, refinement, and proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall Inc, Upper Saddle River (1996)"},{"key":"9589_CR60","unstructured":"Zhang, J., Zhang, H.: System description: generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - CADE-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 (1996). 1007\/3-540-61511-3\\_96"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09589-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09589-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09589-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T07:10:31Z","timestamp":1624518631000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09589-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,5]]},"references-count":60,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["9589"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09589-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,4,5]]},"assertion":[{"value":"30 May 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}