### 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 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 language | English (US) |
---|---|

Title of host publication | Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings |

Pages | 366-382 |

Number of pages | 17 |

DOIs | |

State | Published - 2009 |

Event | 7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 - Trento, Italy Duration: Sep 16 2009 → Sep 18 2009 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 5749 LNAI |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 |
---|---|

Country | Italy |

City | Trento |

Period | 9/16/09 → 9/18/09 |

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

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

## Cite this

*Frontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings*(pp. 366-382). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5749 LNAI). https://doi.org/10.1007/978-3-642-04222-5_23