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 EPR class of first-order logic with equality (with exists*forall* quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints.


Editeur(s):
Ghilardi, Silvio
Sebastiani, Roberto
Publié dans:
Proceedings of the 7th International Symposium on Frontiers of Combining Systems, 366-382
Présenté à:
7th International Symposium on Frontiers of Combining Systems, Trento, Italy, September 16-18, 2009
Année
2009
Publisher:
Springer
Mots-clefs:
Laboratoires:




 Notice créée le 2010-12-01, modifiée le 2019-08-12

n/a:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)