Combining Theories with Shared Set Operations

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¨onfinkel-Ramsey class of first-order logic with equality (with ∃∗ ∀∗ quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints.

• Type: Conference
• Year: 2009
• Where: FROCOS
• Authors: Thomas Wies, Ruzica Piskac, Viktor Kuncak
• Keywords: Control Systems, FROCOS 2009, Monadic Second-order Logic, Monadic Second-order Quantifiers, Share Set Variables