Top

Published in:

2017 | OriginalPaper | Chapter

Decision Procedures for Theories of Sets with Measures

Authors : Markus Bender, Viorica Sofronie-Stokkermans

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 introduce a decision procedure for checking satisfiability of quantifier-free formulae in the combined theory of sets, measures and arithmetic. Such theories are important in mathematics (e.g. probability theory and measure theory) and in applications. We indicate how these ideas can be used for obtaining a decision procedure for a fragment of the duration calculus.

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 Relational Constraint Solving in SMT

next chapter A Decision Procedure for Restricted Intensional Sets

For example, a model in which the set variables \({x}{}_{1}, {x}{}_{2}, {x}{}_{3}\) are interpreted as intervals \(I_1, I_2, I_3\) and the atomic sets \({\mathcal{{S}}{}_{001}}, {\mathcal{{S}}{}_{010}}, {\mathcal{{S}}{}_{100}}, {\mathcal{{S}}{}_{111}}\) are assigned non-empty values and the other atomic intervals are empty, is inconsistent: There can be no section in which the intervals overlap (\(\mathcal{{S}}{}_{111}\) not empty) that is joined by three sections where every set is disjoint from the other two (\({\mathcal{{S}}{}_{001}}, {\mathcal{{S}}{}_{010}},{\mathcal{{S}}{}_{100}}\) are not empty).

Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 65–81. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_6

Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 82–98. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_7

Bender, M.: Reasoning with sets and sums of sets. In: King, T., Piskac, R. (eds.) SMT@IJCAR 2016, Proceedings. CEUR Workshop Proceedings, vol. 1617, pp. 61–70. CEUR-WS.org (2016)

Bouajjani, A., Lakhnech, Y., Robbana, R.: From duration calculus to linear hybrid automata. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 196–210. Springer, Heidelberg (1995). doi:10.1007/3-540-60045-0_51 CrossRef

Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Berlin (2004)CrossRefMATH

Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993). doi:10.1007/3-540-56503-5_8 CrossRef

Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)MathSciNetCrossRefMATH

Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 36–59. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_23 CrossRef

Chetcuti-Sperandio, N.: Tableau-based automated deduction for duration calculus. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS, vol. 2381, pp. 53–69. Springer, Heidelberg (2002). doi:10.1007/3-540-45616-3_5 CrossRef

10.

Chetcuti-Sperandio, N., del Cerro, L.F.: A decision method for duration calculus. J. UCS 5(11), 743–764 (1999)MathSciNetMATH

11.

Chetcuti-Sperandio, N., del Cerro, L.F.: A mixed decision method for duration calculus. J. Log. Comput. 10(6), 877–895 (2000)MathSciNetCrossRefMATH

12.

Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 122–136. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_9

13.

Fränzle, M., Hansen, M.R.: Deciding an interval logic with accumulated durations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 201–215. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_17 CrossRef

14.

Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 30–45. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_4 CrossRef

15.

Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368–382. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_29 CrossRef

16.

Kapur, D., Zarba, C.G.: A reduction approach to decision procedures (2005). https://www.cs.unm.edu/~kapur/mypapers/reduction.pdf,. Unpublished manuscript

17.

Khachiyan, L.: A polynomial algorithm in linear programming. Soviet Math. Dokl. 20(1), 191–194 (1979)MathSciNetMATH

18.

Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 260–277. Springer, Heidelberg (2005). doi:10.1007/11532231_20 CrossRef

19.

Kuncak, V., Nguyen, H.H., Rinard, M.C.: Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reasoning 36(3), 213–239 (2006)MathSciNetCrossRefMATH

20.

Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34–48. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15205-4_5 CrossRef

21.

Ohlbach, H.J.: Set description languages and reasoning about numerical features of sets. In: Lambrix, P., Borgida, A., Lenzerini, M., Möller, R., Patel-Schneider, P.F. (eds.) International Workshop on Description Logics (DL 1999), Proceedings. CEUR Workshop Proceedings, vol. 22. CEUR-WS.org (1999)

22.

Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 219–234. Springer, Heidelberg (2005). doi:10.1007/11532231_16 CrossRef

23.

Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. Multiple-Valued Logic Soft Comput. 13(4–6), 397–414 (2007)MathSciNetMATH

24.

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

25.

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). doi:10.1007/978-3-642-11319-2_27 CrossRef

26.

Zarba, C.G.: Combining sets with cardinals. J. Autom. Reasoning 34(1), 1–29 (2005)MathSciNetCrossRefMATH

27.

Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Gupta, R., Amarasinghe, S.P. (eds.), Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 349–361. ACM (2008)

28.

Chaochen, Z., Jingzhong, Z., Lu, Y., Xiaoshan, L.: Linear duration invariants. In: Langmaack, H., Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994). doi:10.1007/3-540-58468-4_161 CrossRef

Title: Decision Procedures for Theories of Sets with Measures
Authors: Markus Bender
Viorica Sofronie-Stokkermans
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_11

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