Combining theories with shared set operations

Wies T, Piskac R, Kuncak V. 2009. Combining theories with shared set operations. 7th International Symposium on Frontiers of Combining Systems. FroCoS: Frontiers of Combining Systems, LNCS, vol. 5749, 366–382.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English

Scopus indexed
Author
Wies, ThomasISTA; Piskac, Ruzica; Kuncak, Viktor
Series Title
LNCS
Abstract
Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas obtained by applying propositional connectives to formulas belonging to: 1) Boolean Algebra with Presburger Arithmetic (with quantifiers over sets and integers), 2) weak monadic second-order logic over trees (with monadic second-order quantifiers), 3) two-variable logic with counting quantifiers (ranging over elements), 4) the Bernays-Schönfinkel-Ramsey class of first-order logic with equality (with ∃ * ∀ * quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints.
Publishing Year
Date Published
2009-01-01
Proceedings Title
7th International Symposium on Frontiers of Combining Systems
Publisher
Springer
Volume
5749
Page
366 - 382
Conference
FroCoS: Frontiers of Combining Systems
Conference Location
Trento, Italy
Conference Date
2009-09-16 – 2009-09-18
IST-REx-ID

Cite this

Wies T, Piskac R, Kuncak V. Combining theories with shared set operations. In: 7th International Symposium on Frontiers of Combining Systems. Vol 5749. Springer; 2009:366-382. doi:10.1007/978-3-642-04222-5_23
Wies, T., Piskac, R., & Kuncak, V. (2009). Combining theories with shared set operations. In 7th International Symposium on Frontiers of Combining Systems (Vol. 5749, pp. 366–382). Trento, Italy: Springer. https://doi.org/10.1007/978-3-642-04222-5_23
Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with Shared Set Operations.” In 7th International Symposium on Frontiers of Combining Systems, 5749:366–82. Springer, 2009. https://doi.org/10.1007/978-3-642-04222-5_23.
T. Wies, R. Piskac, and V. Kuncak, “Combining theories with shared set operations,” in 7th International Symposium on Frontiers of Combining Systems, Trento, Italy, 2009, vol. 5749, pp. 366–382.
Wies T, Piskac R, Kuncak V. 2009. Combining theories with shared set operations. 7th International Symposium on Frontiers of Combining Systems. FroCoS: Frontiers of Combining Systems, LNCS, vol. 5749, 366–382.
Wies, Thomas, et al. “Combining Theories with Shared Set Operations.” 7th International Symposium on Frontiers of Combining Systems, vol. 5749, Springer, 2009, pp. 366–82, doi:10.1007/978-3-642-04222-5_23.

Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar