Solving quantifier-free first-order constraints over finite sets and binary relations. (English) Zbl 1468.03009

Cristiá, Maximiliano; Rossi, Gianfranco

J. Autom. Reasoning 64, No. 2, 295-330 (2020).

Summary: 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.

MSC:

03B35	Mechanization of proofs and logical operations
68N17	Logic programming
68V15	Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Keywords:

set constraints; binary relations; set-relation algebra; satisfiability solver; automated theorem proving

Software:

Prover9; ProB; Cardinal; Z/EVES; Kodkod; Why3; Isabelle/HOL; Alloy; CPGraph; Mace4; RelView; TPTP; Coq

References:

[1]	Andréka, H.; Givant, Sr; Németi, I., Decision Problems for Equational Theories of Relation Algebras (1997), Providence: American Mathematical Society, Providence · Zbl 0877.03030
[2]	Arias, Ejg; Lipton, J.; Mariño, J., Constraint logic programming with a relational machine, For. Asp. Comput., 29, 1, 97-124 (2017) · Zbl 1355.68035
[3]	Armstrong, Alasdair; Struth, Georg; Weber, Tjark, Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL, Interactive Theorem Proving, 197-212 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1317.68201
[4]	Azevedo, F., Cardinal: a finite sets constraint solver, Constraints, 12, 1, 93-129 (2007) · Zbl 1118.68653
[5]	Berghammer, R.: Relview. http://www.informatik.uni-kiel.de/ progsys/relview/ · Zbl 0800.68963
[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]	Berghammer, Rudolf; Höfner, Peter; Stucke, Insa, Automated Verification of Relational While-Programs, Relational and Algebraic Methods in Computer Science, 173-190 (2014), Cham: Springer International Publishing, Cham · Zbl 1405.68070
[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]	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]	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)
[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.; Omodeo, Eg; Policriti, A., Set Theory for Computing—from Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science (2001), Berlin: Springer, Berlin · Zbl 0981.03056
[13]	Cantone, D.; Schwartz, Jt, 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) · Zbl 0734.03004
[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)
[15]	Clearsy: Aterlier B home page. http://www.atelierb.eu/
[16]	Conchon, S.; Iguernlala, M., Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, 243-253 (2016), Cham: Springer, Cham
[17]	Coq Development Team: The Coq proof assistant reference manual, version 8.8.1. LogiCal Project, Palaiseau (2018)
[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 · Zbl 1411.68060
[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]	Cristiá, Maximiliano; Rossi, Gianfranco, A Decision Procedure for Sets, Binary Relations and Partial Functions, Computer Aided Verification, 179-198 (2016), Cham: Springer International Publishing, Cham · Zbl 1411.68060
[21]	Cristiá, Maximiliano; Rossi, Gianfranco, A Decision Procedure for Restricted Intensional Sets, Automated Deduction - CADE 26, 185-201 (2017), Cham: Springer International Publishing, Cham · Zbl 1496.03041
[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]	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]	Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia, {log} as a Test Case Generator for the Test Template Framework, Software Engineering and Formal Methods, 229-243 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[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]	Déharbe, D.; Fontaine, P.; Guyot, Y.; Voisin, L., Integrating SMT solvers in rodin, Sci. Comput. Program., 94, 130-143 (2014)
[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)
[28]	De Moura, Leonardo, Automated Deduction - CADE 26 (2017), Cham: Springer International Publishing, Cham · Zbl 1369.68037
[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). 10.1109/FMCAD.2009.5351142
[30]	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
[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]	Dovier, A.; Pontelli, E.; Rossi, G., Set unification, Theory Pract. Log. Program., 6, 6, 645-701 (2006) · Zbl 1108.68104
[33]	Gervet, C., Interval propagation to reason about sets: definition and implementation of a practical language, Constraints, 1, 3, 191-244 (1997) · Zbl 0870.68039
[34]	Givant, S., The calculus of relations as a foundation for mathematics, J. Autom. Reasoning, 37, 4, 277-322 (2006) · Zbl 1121.03018
[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]	Hawkins, P.; Lagoon, V.; Stuckey, Pj, Solving set constraint satisfaction problems using ROBDDs, J. Artif. Intell. Res. (JAIR), 24, 109-156 (2005) · Zbl 1080.68666
[37]	Hinman, P.: Fundamentals of Mathematical Logic. CRC Press, Boca Raton (2018). https://books.google.it/books?id=6UBZDwAAQBAJ · Zbl 1081.03003
[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). 10.1007/978-3-540-71070-7_5 · Zbl 1165.68460
[39]	Jackson, Daniel, Alloy: A Logical Modelling Language, ZB 2003: Formal Specification and Development in Z and B, 1-1 (2003), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1028.68548
[40]	Jackson, D., Software Abstractions: Logic, Language, and Analysis (2006), Cambridge: The MIT Press, Cambridge
[41]	Kahl, W., Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types, J. Log. Algebra Program., 76, 1, 60-89 (2008) · Zbl 1139.18005
[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)
[43]	Leuschel, Michael; Butler, Michael, ProB: A Model Checker for B, FME 2003: Formal Methods, 855-874 (2003), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[44]	McCune, W.: Prover9 and mace4 (2005-2010). http://www.cs.unm.edu/ mccune/prover9/
[45]	Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark, Relational Constraint Solving in SMT, Automated Deduction - CADE 26, 148-165 (2017), Cham: Springer International Publishing, Cham · Zbl 1494.68289
[46]	Mentré, David; Marché, Claude; Filliâtre, Jean-Christophe; Asuka, Masashi, Discharging Proof Obligations from Atelier B Using Multiple Automated Provers, Abstract State Machines, Alloy, B, VDM, and Z, 238-251 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[47]	Nipkow, T.; Paulson, Lc; Wenzel, M., Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[48]	Rossi, G.: \(\{\log \} (2008)\). http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html
[49]	Saaltink, M.: The Z/EVES mathematical toolkit version 2.2 for Z/EVES version 1.5. Techical Report, ORA Canada (1997)
[50]	Saaltink, M.; Bowen, Jp; Hinchey, Mg; Till, D., The Z/EVES system, ZUM. Lecture Notes in Computer Science, 72-85 (1997), Berlin: Springer, Berlin
[51]	Schmidt, G.; Hattensperger, C.; Winter, M., Heterogeneous Relation Algebra, 39-53 (1997), Vienna: Springer, Vienna · Zbl 0961.03061
[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) · Zbl 1185.68636
[53]	Tarski, A., On the calculus of relations, J. Symb. Log., 6, 3, 73-89 (1941) · JFM 67.0973.02
[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). 10.1007/978-3-540-71209-1_49
[55]	Zhang, Jian; Zhang, Hantao, System description generating models by SEM, Automated Deduction — Cade-13, 308-312 (1996), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1412.68268