Decision Procedures for Power Structures

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction of Hintikka formulae is not necessary in the quantifier-free case. We show that the result stays true when the theory of the indices is enriched with a finiteness or an order predicate. We prove that the resulting logical fragment gives quantifier-free logics suitable for verification. We conclude by applying the developed techniques to the existential fragment of the theory of non-linear integer arithmetic and the theory of arrays.