Name
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 ∃*¬* quantifier prefix), and 5) the quantifier-free logic of multisets with cardinality constraints. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04222-5_23 | FroCos |
Keywords | Field | DocType |
combining theory,nfinkel-ramsey class,two-variable logic,combination theorem,quantifier-free logic,non-disjoint combination,monadic second-order quantifiers,weak monadic second-order logic,boolean algebra,first-order logic,presburger arithmetic,first order logic,automated reasoning,satisfiability,languages,combination,software verification | Discrete mathematics,Predicate variable,Second-order logic,Zeroth-order logic,Algorithm,Decidability,First-order logic,Boolean algebra,Predicate logic,Mathematics,Monadic predicate calculus | Conference |
Volume | ISSN | ISBN |
5749 | 0302-9743 | 3-642-04221-X |
Citations | PageRank | References |
21 | 0.77 | 30 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Wies | 1 | 515 | 28.26 |
| Ruzica Piskac | 2 | 373 | 24.47 |
| Viktor Kuncak | 3 | 1129 | 70.57 |