Top

Published in:

2017 | OriginalPaper | Chapter

A Decision Procedure for Restricted Intensional Sets

Authors : Maximiliano Cristiá, Gianfranco Rossi

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In this paper we present a decision procedure for Restricted Intensional Sets (RIS), i.e. sets given by a property rather than by enumerating their elements, similar to set comprehensions available in specification languages such as B and Z. The proposed procedure is parametric with respect to a first-order language and theory \(\mathcal {X}\), providing at least equality and a decision procedure to check for satisfiability of \(\mathcal {X}\)-formulas. We show how this framework can be applied when \(\mathcal {X}\) is the theory of hereditarily finite sets as is supported by the language CLP(\(\mathcal {SET}\)). We also present a working implementation of RIS as part of the \(\{log\}\) tool and we show how it compares with a mainstream solver and how it helps in the automatic verification of code fragments.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 102.000 Bücher
über 537 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 Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Decision Procedures for Theories of Sets with Measures

next chapter Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints

The form of RIS terms is borrowed from the form of set comprehension expressions available in Z.

This is guaranteed by procedure remove_neq (see Sect. 3).

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

Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_8 CrossRef

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

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)

Cristiá, M., Rossi, G.: Restricted insentional sets. http://people.dmi.unipr.it/gianfranco.rossi/SETLOG/risCADEonline.pdf

Cristiá, M., Rossi, G.: A decision procedure for sets, binary relations and partial functions. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part I. LNCS, vol. 9779, pp. 179–198. Springer, Cham (2016). doi:10.1007/978-3-319-41528-4_10

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, PPDP 2003, pp. 219–229. ACM, New York (2003). http://doi.acm.org/10.1145/888251.888272

Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules for SMT proofs. In: Workshop on Proof eXchange for Theorem Proving (2011)

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). http://dx.doi.org/10.1016/0743-1066(95)00147-6

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

10.

Dovier, A., Pontelli, E., Rossi, G.: Intensional sets in CLP. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 284–299. Springer, Heidelberg (2003). doi:10.1007/978-3-540-24599-5_20 CrossRef

11.

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

12.

Drăgoi, 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.) VMCAI 2014. LNCS, vol. 8318, pp. 161–181. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_10 CrossRef

13.

Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25 CrossRef

14.

Hill, P.M., Lloyd, J.W.: The Gödel Programming Language. MIT Press, Cambridge (1994)MATH

15.

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

16.

Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45236-2_46 CrossRef

17.

Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_38 CrossRef

18.

Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_42 CrossRef

19.

Rossi, G.: \(\{log\}\) (2008). http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html

20.

Schneider, S.: The B-method: An Introduction. Cornerstones of Computing. Palgrave (2001). http://books.google.com.ar/books?id=Krs0OQAACAAJ

21.

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, New York (1986). http://dx.doi.org/10.1007/978-1-4613-9575-1

22.

Veanes, M., Saabas, A.: On bounded reachability of programs with set comprehensions. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 305–317. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89439-1_22 CrossRef

23.

Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366–382. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04222-5_23 CrossRef

24.

Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)MATH

25.

Zhang, J., Zhang, H.: System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 308–312. Springer, Heidelberg (1996). doi:10.1007/3-540-61511-3_96 CrossRef

Title: A Decision Procedure for Restricted Intensional Sets
Authors: Maximiliano Cristiá
Gianfranco Rossi
Publisher: Springer International Publishing
Book: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_12

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner