Combining theories with shared set operations

Thomas Wies, Ruzica Piskac, Viktor Kuncak

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
Number of pages17
StatePublished - 2009
Event7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 - Trento, Italy
Duration: Sep 16 2009Sep 18 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5749 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other7th International Symposium on Frontiers of Combining Systems, FroCoS 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Combining theories with shared set operations'. Together they form a unique fingerprint.

Cite this