Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Termination Analysis of Probabilistic Programs Through Positivstellensatz’s Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

A Decision Procedure for Sets, Binary Relations and Partial Functions

verfasst von : Maximiliano Cristiá, Gianfranco Rossi

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this paper we present a decision procedure for sets, binary relations and partial functions. The language accepted by the decision procedure includes untyped, hereditarily finite sets, where some of their elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Partial functions are encoded as binary relations which in turn are just sets of ordered pairs. Sets are first-class entities in the language, thus they are not encoded in lower level theories. The decision procedure exploits set unification and set constraint solving as primitive features. The procedure is proved to be sound, complete and terminating. A Prolog implementation is presented.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
Nächstes Kapitel Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
Fußnoten
1
From now on, the term ‘set’ will always include binary relations and partial functions and the term ‘binary relation’ will include partial functions, unless stated differently.
 
2
In the rest of the paper we will use \(R, S, T, \dots \) for relations; \(f, g, h, \dots \) for functions; \(A, B, C, \dots \) for sets; \(t, u, v, w, x, y, z, \dots \) for any other object.
 
3
\( diff (A,B,C)\) holds iff \(C = A \setminus B\); and \( inters (A,B,C)\) holds iff \(C = A \cap B\).
 
4
More precisely, each solution of C expanded to the variables occurring in \(C_{i}\) but not in C, so to account for the possible fresh variables introduced into \(C_{i}\).
 
Literatur
1.
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000)CrossRef
2.
Cristiá, M., Rossi, G., Frydman, C.: \(\{log\}\) as a test case generator for the test template framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 229–243. Springer, Heidelberg (2013)CrossRef
3.
Cristiá, M., Rossi, G., Frydman, C.S.: Adding partial functions to constraint logic programming with sets. TPLP 15(4–5), 651–665 (2015)MathSciNet
4.
5.
Dovier, A., Policriti, A., Rossi, G.: A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inform. 36(2–3), 201–234 (1998)MathSciNetMATH
6.
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefMATH
7.
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)MATH
8.
9.
10.
Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Trans. Softw. Eng. 22(11), 777–793 (1996)CrossRef
11.
Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing - From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, New York (2001)MATH
12.
Calvanese, D., De Giacomo, G.: Expressive description logics. In: Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.) The Description Logic Handbook: Theory, Implementation, and Applications, pp. 178–218. Cambridge University Press, Cambridge (2003)
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)MathSciNetMATH
14.
Zarba, C.G., Cantone, D., Schwartz, J.T.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, I: the two-level case. J. Autom. Reason. 33(3–4), 251–269 (2004)MathSciNetCrossRefMATH
15.
Cantone, D., Zarba, C.G., Cannata, R.R.: A tableau-based decision procedure for a fragment of set theory with iterated membership. J. Autom. Reason. 34(1), 49–72 (2005)MathSciNetCrossRefMATH
16.
Marnette, B., Kuncak, V., Rinard, M.: Polynomial constraints for sets with cardinality bounds. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 258–273. Springer, Heidelberg (2007)CrossRef
17.
18.
Gervet, C.: Interval propagation to reason about sets: definition and implementation of a practical language. Constraints 1(3), 191–244 (1997)MathSciNetCrossRefMATH
19.
Hawkins, P., Lagoon, V., Stuckey, P.J.: Solving set constraint satisfaction problems using ROBDDs. J. Artif. Intell. Res. (JAIR) 24, 109–156 (2005)CrossRefMATH
20.
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)
21.
Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.4pl6. LogiCal Project, Palaiseau, France (2014)
22.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
23.
Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)CrossRef
24.
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 of the 7th International Workshop on Satisfiability Modulo Theories at CADE 22 (2009)
25.
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, Austin, Texas, USA, 15–18 November 2009, pp. 45–52. IEEE (2009)
26.
Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94, 130–143 (2014)CrossRef
27.
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., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238–251. Springer, Heidelberg (2012)CrossRef
28.
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)
29.
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)
30.
31.
Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 380–395. Springer, Heidelberg (2010)CrossRef
Metadaten
Titel
A Decision Procedure for Sets, Binary Relations and Partial Functions
verfasst von
Maximiliano Cristiá
Gianfranco Rossi
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41528-4_10