TY - GEN
T1 - Combining theories with shared set operations
AU - Wies, Thomas
AU - Piskac, Ruzica
AU - Kuncak, Viktor
PY - 2009
Y1 - 2009
N2 - 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 ∃* ∀z.ast; quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints.
AB - 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 ∃* ∀z.ast; quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints.
UR - http://www.scopus.com/inward/record.url?scp=76749121561&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=76749121561&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-04222-5_23
DO - 10.1007/978-3-642-04222-5_23
M3 - Conference contribution
AN - SCOPUS:76749121561
SN - 364204221X
SN - 9783642042218
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 366
EP - 382
BT - Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
T2 - 7th International Symposium on Frontiers of Combining Systems, FroCoS 2009
Y2 - 16 September 2009 through 18 September 2009
ER -