paper ps
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 EPR class of
first-order logic with equality (with exists*forall* quantifier prefix),
and 5) the quantifier-free logic of
multisets with cardinality constraints.

### Citation

Thomas Wies, Ruzica Piskac, and Viktor Kuncak.
Combining theories with shared set operations.
In *FroCoS: Frontiers in Combining Systems*, 2009.### BibTex Entry

@inproceedings{WiesETAL09CombiningTheorieswithSharedSetOperations,
author = {Thomas Wies and Ruzica Piskac and Viktor Kuncak},
title = {Combining Theories with Shared Set Operations},
booktitle = {FroCoS: Frontiers in Combining Systems},
year = 2009,
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 EPR class of
first-order logic with equality (with exists*forall* quantifier prefix),
and 5) the quantifier-free logic of
multisets with cardinality constraints.}
}