×

Automated reasoning with restricted intensional sets. (English) Zbl 07432188

Summary: Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification languages such as B and Z). Notwithstanding, very few tools exist supporting high-level automated reasoning on general formulas involving intensional sets. In this paper we present a decision procedure for a first-order logic language offering both extensional and (a restricted form of) intensional sets (RIS). RIS are introduced as first-class citizens of the language, and set-theoretical operators on RIS are dealt with as constraints. Syntactic restrictions on RIS guarantee that the denoted sets are finite. The language of RIS, called \({\mathcal{L}}_\mathcal{RIS} \), is parametric with respect to any first-order theory \({\mathcal{X}}\) providing at least equality and a decision procedure for \({\mathcal{X}} \)-formulas. In particular, we consider the instance of \({\mathcal{L}}_\mathcal{RIS}\) when \({\mathcal{X}}\) is the theory of hereditarily finite sets and binary relations. We also present a working implementation of this instance as part of the \(\{log\}\) tool, and we show through a number of examples and two case studies that, although RIS are a subclass of general intensional sets, they are still sufficiently expressive as to encode and solve many interesting problems. Finally, an extensive empirical evaluation provides evidence that the tool can be used in practice.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Abrial, JR, The B-book: Assigning Programs to Meanings (1996), New York: Cambridge University Press, New York · Zbl 0915.68015
[2] Barbuti, R.; Mancarella, P.; Pedreschi, D.; Turini, F., A transformational approach to negation in logic programming, J. Log. Program., 8, 3, 201-228 (1990) · Zbl 0796.68056
[3] Beeri, C.; Naqvi, SA; Shmueli, O.; Tsur, S., Set constructors in a logic database language, J. Log. Program., 10, 3-4, 181-232 (1991) · Zbl 0724.68016
[4] Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical foundations. MTR 2547, The MITRE Corporation (1973)
[5] Bell, D.E., LaPadula, L.: Secure computer systems: Mathematical model. ESD-TR 73-278, The MITRE Corporation (1973)
[6] Bjørner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7935, pp. 105-125. Springer (2013). 1007/978-3-642-38856-9_8
[7] 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-18, 1994. pp. 647-661. MIT Press (1994)
[8] 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-1050 (2020) · Zbl 1468.68282
[9] Cabalar, P.; Fandinno, J.; del Cerro, LF; Pearce, D., Functional ASP with intensional sets: application to Gelfond-Zhang aggregates, Theory Pract. Log. Program., 18, 3-4, 390-405 (2018) · Zbl 1451.68255
[10] Cantone, D.; Ferro, A.; Omodeo, E., Computable Set Theory (1989), USA: Clarendon Press, USA · Zbl 0755.03024
[11] 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-325 (2014) · Zbl 1329.03045
[12] 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-159. Springer (2000). 1007/10722086_14 · Zbl 0963.03018
[13] Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model building. In: CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications. pp. 11-27 (2003)
[14] Clearsy: Aterlier B home page, http://www.atelierb.eu/
[15] Conchon, S., Iguernlala, M.: Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, pp. 243-253. Springer, Cham (2016). 1007/978-3-319-33951-1_18
[16] Cristiá, 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
[17] Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) Automated Deduction - CADE 26-26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185-201. Springer (2017), 1007/978-3-319-63046-5_12 · Zbl 06778404
[18] Cristiá, 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-349. Springer (2018). 1007/978-3-030-02149-8_20 · Zbl 06975218
[19] Cristiá, 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 · Zbl 1411.68060
[20] Cristiá, M., Rossi, G.: Automated proof of Bell-LaPadula security properties. J. Autom. Reasoning n/a(n/a) (jul 2020), https://link.springer.com/article/10.1007/s10817-020-09577-6 · Zbl 07356979
[21] Cristiá, M., Rossi, G.: An automatically verified prototype of the Tokeneer ID station specification. CoRR abs/2009.00999 (2020), https://arxiv.org/abs/2009.00999
[22] Cristiá, M.; Rossi, G., Solving quantifier-free first-order constraints over finite sets and binary relations, J. Autom. Reasoning, 64, 2, 295-330 (2020) · Zbl 1468.03009
[23] Cristiá, 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/
[24] Cristiá, 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-243. Springer (2013)
[25] Cristiá, M.; Rossi, G.; Frydman, CS, Adding partial functions to constraint logic programming with sets, TPLP, 15, 4-5, 651-665 (2015) · Zbl 1379.68053
[26] Dal Palú, 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-229. PPDP ’03, ACM, New York (2003), doi:10.1145/888251.888272
[27] Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules for SMT proofs. In: Workshop on Proof eXchange for Theorem Proving (2011) · Zbl 1341.68187
[28] Delahaye, D., Dubois, C., Marché, C., Mentré, 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-6, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8477, pp. 290-293. Springer (2014). 1007/978-3-662-43652-3_26
[29] Dovier, A.; Omodeo, EG; Pontelli, E.; Rossi, G., A language for programming in logic with finite sets, J. Log. Program., 28, 1, 1-44 (1996) · Zbl 0874.68056
[30] Dovier, A.; Piazza, C.; Pontelli, E.; Rossi, G., Sets and constraint logic programming, ACM Trans. Program. Lang. Syst., 22, 5, 861-931 (2000)
[31] Dovier, A.; Pontelli, E.; Rossi, G., Constructive negation and constraint logic programming with sets, New Gener. Comput., 19, 3, 209-256 (2001) · Zbl 0980.68017
[32] 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-13, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2916, pp. 284-299. Springer (2003). 1007/978-3-540-24599-5_20 · Zbl 1204.68051
[33] Dovier, A.; Pontelli, E.; Rossi, G., Set unification, Theory Pract. Log Program, 6, 6, 645-701 (2006) · Zbl 1108.68104
[34] 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-21, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8318, pp. 161-181. Springer (2014). 1007/978-3-642-54013-4_10 · Zbl 1428.68371
[35] Ferraris, P., Logic programs with propositional connectives and aggregates, ACM Trans. Comput. Log., 12, 4, 25:1-25:40 (2011) · Zbl 1351.68053
[36] Gao, C., Chen, T., Wu, Z.: Separation logic with linearly compositional inductive predicates and set data constraints. In: Catania, B., Královic, 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ý Smokovec, Slovakia, January 27-30, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11376, pp. 206-220. Springer (2019). 1007/978-3-030-10801-4_17
[37] Ge, Y., de Moura, 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-July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 306-320. Springer (2009). 1007/978-3-642-02658-4_25 · Zbl 1242.68280
[38] Gebser, M.; Harrison, A.; Kaminski, R.; Lifschitz, V.; Schaub, T., Abstract gringo, Theory Pract. Log Program, 15, 4-5, 449-463 (2015) · Zbl 1379.68031
[39] Hill, PM; Lloyd, JW, The Gödel Programming Language (1994), Cambridge: MIT Press, Cambridge · Zbl 0850.68138
[40] Jackson, D., Software Abstractions: Logic, Language, and Analysis (2006), Cambridge: The MIT Press, Cambridge
[41] Lam, E.S.L., Cervesato, I.: Reasoning about set comprehensions. In: Rümmer, 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-18, 2014. CEUR Workshop Proceedings, vol. 1163, pp. 27-37. CEUR-WS.org (2014), http://ceur-ws.org/Vol-1163/paper-05.pdf
[42] 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-874. Springer (2003)
[43] Mammar, A.; Laleau, R., Modeling a landing gear system in event-b, Int. J. Softw. Tools Technol. Transf., 19, 2, 167-186 (2017)
[44] Mentré, D., Marché, C., Filliâtre, 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-251. Springer (2012)
[45] Merz, S.; Vanzetto, H., Encoding tla \({}^{\text{+}}\) into unsorted and many-sorted first-order logic, Sci. Comput. Program., 158, 3-20 (2018)
[46] 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-426. Springer (2000). 1007/3-540-44622-2_28 · Zbl 0973.68039
[47] 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-27, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4741, pp. 529-543. Springer (2007). 1007/978-3-540-74970-7_38
[48] 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-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 640-655. Springer (2013). 1007/978-3-642-39799-8_42 · Zbl 1381.68275
[49] Rossi, G.: \(\{log\}\). http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html (2008), http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html
[50] Rossi, G.; Panegai, E.; Poleo, E., Jsetl: a java library for supporting declarative programming in java, Softw. Pract. Exp., 37, 2, 115-149 (2007)
[51] 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-85. Springer (1997)
[52] Schneider, S.: The B-method: An Introduction. Cornerstones of computing, Palgrave (2001), http://books.google.com.ar/books?id=Krs0OQAACAAJ
[53] 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), doi:10.1007/978-1-4613-9575-1 · Zbl 0604.68001
[54] Son, TC; Pontelli, E., A constructive semantic characterization of aggregates in answer set programming, Theory Pract. Log. Program., 7, 3, 355-375 (2007) · Zbl 1111.68072
[55] Spivey, JM, The Z Notation: A Reference Manual (1992), Hertfordshire: Prentice Hall International (UK) Ltd.,, Hertfordshire · Zbl 0777.68003
[56] Sutcliffe, G., The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0, J. Autom. Reason., 43, 4, 337-362 (2009) · Zbl 1185.68636
[57] 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-27, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5330, pp. 305-317. Springer (2008). 1007/978-3-540-89439-1_22 · Zbl 1182.68048
[58] 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-18, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5749, pp. 366-382. Springer (2009). 1007/978-3-642-04222-5_23 · Zbl 1193.03030
[59] Woodcock, J.; Davies, J., Using Z: specification, refinement, and proof (1996), Upper Saddle River: Prentice-Hall Inc, Upper Saddle River · Zbl 0855.68060
[60] 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-August 3, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1104, pp. 308-312. Springer (1996). 1007/3-540-61511-3_96 · Zbl 1412.68268
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.