{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:54Z","timestamp":1740098934443,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_12","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"185-201","source":"Crossref","is-referenced-by-count":10,"title":["A Decision Procedure for Restricted Intensional Sets"],"prefix":"10.1007","author":[{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38856-9_8"},{"key":"12_CR2","doi-asserted-by":"crossref","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). \nhttp:\/\/dx.doi.org\/10.1016\/j.tcs.2014.03.021","journal-title":"Theor. Comput. Sci."},{"key":"12_CR3","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":"12_CR4","unstructured":"Cristi\u00e1, M., Rossi, G.: Restricted insentional sets. \nhttp:\/\/people.dmi.unipr.it\/gianfranco.rossi\/SETLOG\/risCADEonline.pdf"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-41528-4_10","volume-title":"Computer Aided Verification","author":"M 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.) CAV 2016, Part I. LNCS, vol. 9779, pp. 179\u2013198. Springer, Cham (2016). doi:\n10.1007\/978-3-319-41528-4_10"},{"key":"12_CR6","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, PPDP 2003, pp. 219\u2013229. ACM, New York (2003). \nhttp:\/\/doi.acm.org\/10.1145\/888251.888272"},{"key":"12_CR7","unstructured":"Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules for SMT proofs. In: Workshop on Proof eXchange for Theorem Proving (2011)"},{"key":"12_CR8","doi-asserted-by":"crossref","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). \nhttp:\/\/dx.doi.org\/10.1016\/0743-1066(95)00147-6","DOI":"10.1016\/0743-1066(95)00147-6"},{"issue":"5","key":"12_CR9","doi-asserted-by":"crossref","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."},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-540-24599-5_20","volume-title":"Logic Programming","author":"A Dovier","year":"2003","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Intensional sets in CLP. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 284\u2013299. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-24599-5_20"},{"issue":"6","key":"12_CR11","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theor. Pract. Log. Program. 6(6), 645\u2013701 (2006). \nhttp:\/\/dx.doi.org\/10.1017\/S1471068406002730","journal-title":"Theor. Pract. Log. Program."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-54013-4_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Dr\u0103goi","year":"2014","unstructured":"Dr\u0103goi, 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.) VMCAI 2014. LNCS, vol. 8318, pp. 161\u2013181. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54013-4_10"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02658-4_25"},{"key":"12_CR14","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":"12_CR15","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":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45236-2_46"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74970-7_38"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_42"},{"key":"12_CR19","unstructured":"Rossi, G.: \n            $$\\{log\\}$$\n           (2008). \nhttp:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html"},{"key":"12_CR20","unstructured":"Schneider, S.: The B-method: An Introduction. Cornerstones of Computing. Palgrave (2001). \nhttp:\/\/books.google.com.ar\/books?id=Krs0OQAACAAJ"},{"key":"12_CR21","doi-asserted-by":"crossref","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, New York (1986). \nhttp:\/\/dx.doi.org\/10.1007\/978-1-4613-9575-1","DOI":"10.1007\/978-1-4613-9575-1"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-89439-1_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Veanes","year":"2008","unstructured":"Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 305\u2013317. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-89439-1_22"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366\u2013382. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-04222-5_23"},{"key":"12_CR24","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":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-61511-3_96","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Zhang","year":"1996","unstructured":"Zhang, J., Zhang, H.: System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308\u2013312. Springer, Heidelberg (1996). doi:\n10.1007\/3-540-61511-3_96"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:37:10Z","timestamp":1499679430000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}