Advertisement

Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations

  • Maximiliano CristiáEmail author
  • Gianfranco Rossi
Article
  • 9 Downloads

Abstract

In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped, hereditarily finite sets, whose elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Sets are first-class entities in the language, thus they are not encoded in lower level theories. Relations are just sets of ordered pairs. The solver exploits set unification and set constraint solving as primitive features. The solver is proved to be a sound semi-decision procedure for the accepted language. A Prolog implementation is presented and an extensive empirical evaluation provides evidence of its usefulness.

Keywords

Set constraints Binary relations Set relation algebra Satisfiability solver \(\{\log \}\) Automated theorem proving 

Notes

Supplementary material

10817_2019_9520_MOESM1_ESM.pdf (566 kb)
Supplementary material 1 (pdf 565 KB)

References

  1. 1.
    Andréka, H., Givant, S.R., Németi, I.: Decision Problems for Equational Theories of Relation Algebras, vol. 604. American Mathematical Society, Providence (1997)zbMATHGoogle Scholar
  2. 2.
    Arias, E.J.G., Lipton, J., Mariño, J.: Constraint logic programming with a relational machine. For. Asp. Comput. 29(1), 97–124 (2017).  https://doi.org/10.1007/s00165-016-0369-z MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    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—4th International Conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7998, pp. 197–212. Springer, Berlin (2013).  https://doi.org/10.1007/978-3-642-39634-2_16
  4. 4.
    Azevedo, F.: Cardinal: a finite sets constraint solver. Constraints 12(1), 93–129 (2007).  https://doi.org/10.1007/s10601-006-9012-6 CrossRefzbMATHGoogle Scholar
  5. 5.
  6. 6.
    Berghammer, R., Hoffmann, T., Leoniuk, B., Milanese, U.: Prototyping and programming with relations. Electr. Notes Theor. Comput. Sci. 44(3), 27–50 (2001).  https://doi.org/10.1016/S1571-0661(04)80931-9 CrossRefGoogle Scholar
  7. 7.
    Berghammer, R., Höfner, P., Stucke, I.: Automated verification of relational while-programs. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds.) Relational and Algebraic Methods in Computer Science—14th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28–May 1, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8428, pp. 173–190. Springer, Berlin (2014).  https://doi.org/10.1007/978-3-319-06251-8_11
  8. 8.
    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–948 (2004)CrossRefGoogle Scholar
  9. 9.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: 1st International Workshop on Intermediate Verification Languages. Wrocław, Poland (August 2011). http://proval.lri.fr/submissions/boogie11.pdf
  10. 10.
    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–17, 1994, pp. 269–285. MIT Press, Cambridge (1994)Google Scholar
  11. 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).  https://doi.org/10.1016/j.tcs.2014.03.021 MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing—from Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, Berlin (2001).  https://doi.org/10.1007/978-1-4757-3452-2 zbMATHGoogle Scholar
  13. 13.
    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–256 (1991).  https://doi.org/10.1007/BF00243808 MathSciNetzbMATHGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Clearsy: Aterlier B home page. http://www.atelierb.eu/
  16. 16.
    Conchon, S., Iguernlala, M.: Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, pp. 243–253. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33951-1_18 Google Scholar
  17. 17.
    Coq Development Team: The Coq proof assistant reference manual, version 8.8.1. LogiCal Project, Palaiseau (2018)Google Scholar
  18. 18.
    Cristiá, M., Rossi, G.: Rewrite rules for a solver for sets, binary relations and partial functions. http://people.dmi.unipr.it/gianfranco.rossi/SETLOG/calculus.pdf
  19. 19.
    Cristiá, M., Rossi, G.: Rapid prototyping and animation of Z specifications using \(\{\log \}\). In: 1st International Workshop about Sets and Tools (SETS 2014), pp. 4–18 (2014), Informal Proceedings. http://sets2014.cnam.fr/papers/sets2014.pdf
  20. 20.
    Cristiá, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification—28th International Conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9779, pp. 179–198. Springer, Berlin (2016).  https://doi.org/10.1007/978-3-319-41528-4_10
  21. 21.
    Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura [28], pp. 185–201.  https://doi.org/10.1007/978-3-319-63046-5_12
  22. 22.
    Cristiá, M., Rossi, G.: Detailed proofs of \({\cal{L}}_{{\cal{BR}}}\) properties for the paper: “solving quantifier-free first-order constraints over finite sets and binary relations” (2018). https://www.dropbox.com/s/jlisk0vngeb42c3/proofs.pdf?dl=0
  23. 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@CADE 2017, Gothenburg, Sweden, 7th August 2017 (2017). http://software.imdea.org/Conferences/hcvs17/
  24. 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, Berlin (2013)Google Scholar
  25. 25.
    Cristiá, M., Rossi, G., Frydman, C.S.: Adding partial functions to constraint logic programming with sets. TPLP 15(4–5), 651–665 (2015).  https://doi.org/10.1017/S1471068415000290 MathSciNetzbMATHGoogle Scholar
  26. 26.
    Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in rodin. Sci. Comput. Program. 94, 130–143 (2014).  https://doi.org/10.1016/j.scico.2014.04.012 CrossRefGoogle Scholar
  27. 27.
    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–47 (2005)Google Scholar
  28. 28.
    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. Springer, Berlin (2017).  https://doi.org/10.1007/978-3-319-63046-5
  29. 29.
    de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA, pp. 45–52. IEEE, New York (2009).  https://doi.org/10.1109/FMCAD.2009.5351142
  30. 30.
    Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. Log. Program. 28(1), 1–44 (1996).  https://doi.org/10.1016/0743-1066(95)00147-6 MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000)CrossRefGoogle Scholar
  32. 32.
    Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645–701 (2006).  https://doi.org/10.1017/S1471068406002730 MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Gervet, C.: Interval propagation to reason about sets: definition and implementation of a practical language. Constraints 1(3), 191–244 (1997).  https://doi.org/10.1007/BF00137870 MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reasoning 37(4), 277–322 (2006).  https://doi.org/10.1007/s10817-006-9062-x MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Guttmann, W., Struth, G., Weber, T.: A repository for Tarski–Kleene algebras. In: Höfner, P., McIver, A., Struth, G. (eds.) Proceedings of the 5th Workshop on Automated Theory Engineering, Wrocław, Poland, July 31, 2011. CEUR Workshop Proceedings, vol. 760, pp. 30–39. CEUR-WS.org (2011). http://ceur-ws.org/Vol-760/paper5.pdf
  36. 36.
    Hawkins, P., Lagoon, V., Stuckey, P.J.: Solving set constraint satisfaction problems using ROBDDs. J. Artif. Intell. Res. (JAIR) 24, 109–156 (2005).  https://doi.org/10.1613/jair.1638 CrossRefzbMATHGoogle Scholar
  37. 37.
    Hinman, P.: Fundamentals of Mathematical Logic. CRC Press, Boca Raton (2018). https://books.google.it/books?id=6UBZDwAAQBAJ
  38. 38.
    Höfner, 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–15, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 50–66. Springer, Berlin (2008).  https://doi.org/10.1007/978-3-540-71070-7_5
  39. 39.
    Jackson, D.: Alloy: A logical modelling language. In: Bert, D., Bowen, J.P., King, S., Waldén, 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–6, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2651, p. 1. Springer, Berlin (2003).  https://doi.org/10.1007/3-540-44880-2_1
  40. 40.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar
  41. 41.
    Kahl, W.: Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types. J. Log. Algebra Program. 76(1), 60–89 (2008).  https://doi.org/10.1016/j.jlap.2007.10.008 MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Kröning, D., Rümmer, 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)Google Scholar
  43. 43.
    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, Berlin (2003)Google Scholar
  44. 44.
    McCune, W.: Prover9 and mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9/
  45. 45.
    Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de Moura [28], pp. 148–165.  https://doi.org/10.1007/978-3-319-63046-5_10
  46. 46.
    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, Berlin (2012)Google Scholar
  47. 47.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002)zbMATHGoogle Scholar
  48. 48.
  49. 49.
    Saaltink, M.: The Z/EVES mathematical toolkit version 2.2 for Z/EVES version 1.5. Techical Report, ORA Canada (1997)Google Scholar
  50. 50.
    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, Berlin (1997)Google Scholar
  51. 51.
    Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous Relation Algebra, pp. 39–53. Springer, Vienna (1997).  https://doi.org/10.1007/978-3-7091-6510-2_3 zbMATHGoogle Scholar
  52. 52.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941).  https://doi.org/10.2307/2268577 MathSciNetCrossRefzbMATHGoogle Scholar
  54. 54.
    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–April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4424, pp. 632–647. Springer, Berlin (2007).  https://doi.org/10.1007/978-3-540-71209-1_49
  55. 55.
    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, Berlin (1996).  https://doi.org/10.1007/3-540-61511-3_96

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.Universidad Nacional de Rosario and CIFASISRosarioArgentina
  2. 2.Università di ParmaParmaItaly

Personalised recommendations