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

• Maximiliano Cristiá
• Gianfranco Rossi
Article

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

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)
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).
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).
4. 4.
Azevedo, F.: Cardinal: a finite sets constraint solver. Constraints 12(1), 93–129 (2007).
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).
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).
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)
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).
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).
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).
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.
16. 16.
Conchon, S., Iguernlala, M.: Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, pp. 243–253. Springer, Cham (2016). 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).
21. 21.
Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura [28], pp. 185–201.
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).
26. 26.
Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in rodin. Sci. Comput. Program. 94, 130–143 (2014).
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).
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).
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).
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)
32. 32.
Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645–701 (2006).
33. 33.
Gervet, C.: Interval propagation to reason about sets: definition and implementation of a practical language. Constraints 1(3), 191–244 (1997).
34. 34.
Givant, S.: The calculus of relations as a foundation for mathematics. J. Autom. Reasoning 37(4), 277–322 (2006).
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).
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).
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).
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).
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.
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)
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).
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)
53. 53.
Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941).
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).
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).