Combining Theories with Shared Set Operations

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.}
}