nach oben

Tipp

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

verfasst von: Maximiliano Cristiá, Gianfranco Rossi

Erschienen in: Journal of Automated Reasoning

Einloggen, um Zugang zu erhalten

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.

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Nur mit Berechtigung zugänglich

More precisely, each solution of \(\varPhi \) expanded to the variables occurring in \(\varPhi _i\) but not in \(\varPhi \), so as to account for the possible fresh variables introduced into \(\varPhi _i\).

Actually there is some overlapping among these collections. This is difficult to avoid, as each author uses different variable names, the problem can be stated in slightly different ways (e.g., by applying commutativity) and even different names for the same operator are used (e.g., sum and union).

Most of the time is spent in solving 27 problems of tptp.bool encoding rather complex Boolean results where instead of using Boolean variables, we prove more general results by using finite set variables.

Andréka, H., Givant, S.R., Németi, I.: Decision Problems for Equational Theories of Relation Algebras, vol. 604. American Mathematical Society, Providence (1997) MATH

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 MathSciNetCrossRefMATH

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 CrossRef

Azevedo, F.: Cardinal: a finite sets constraint solver. Constraints 12(1), 93–129 (2007). https://doi.org/10.1007/s10601-006-9012-6 CrossRefMATH

Berghammer, R.: Relview. http://www.informatik.uni-kiel.de/~progsys/relview/

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 CrossRef

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 CrossRef

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) CrossRef

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). https://doi.org/10.1016/j.tcs.2014.03.021 MathSciNetCrossRefMATH

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 CrossRefMATH

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 MathSciNetCrossRefMATH

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, pp. 243–253. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_18 CrossRef

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

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á, 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 CrossRef

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 CrossRef

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á, 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) CrossRef

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 MathSciNetCrossRefMATH

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 CrossRef

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, 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 MATH

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.

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 MathSciNetCrossRefMATH

31.

Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000) CrossRef

32.

Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645–701 (2006). https://doi.org/10.1017/S1471068406002730 MathSciNetCrossRefMATH

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 MathSciNetCrossRefMATH

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 MathSciNetCrossRefMATH

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, 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 CrossRefMATH

37.

Hinman, P.: Fundamentals of Mathematical Logic. CRC Press, Boca Raton (2018). https://books.google.it/books?id=6UBZDwAAQBAJ

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.

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.

Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)

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 MathSciNetCrossRefMATH

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, 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) CrossRef

44.

McCune, W.: Prover9 and mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9/

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 CrossRef

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) CrossRef

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) MATH

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

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 CrossRefMATH

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) MathSciNetCrossRef

53.

Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941). https://doi.org/10.2307/2268577 MathSciNetCrossRefMATH

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.

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 CrossRef

Titel: Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations
verfasst von: Maximiliano Cristiá
Gianfranco Rossi
Publikationsdatum: 08.04.2019
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-019-09520-4

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

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

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner