[ list |
abstracts |
bib ]

## Combining Theories with Shared Set Operations

paper pdf
paper ps
### 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.

### 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,
localurl = {http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.pdf}
}

[ list |
abstracts |
bib ]