Dominoes and the complexity of subclasses of logical theories (Q1115859)

The complexity of classes of quantifier prefix bounded formulas in logical theories (mainly Presburger and Skolem arithmetic) is studied. The main result for Presburger arithmetic is exponential time complexity for \(\exists \forall^*\)-formulas. Main results for Skolem arithmetic are: 1) NP-completeness of the class of \(\exists^*\)-formulas, 2) NP- completeness of the class of \(\exists\)-formulas if the divisibility relation is allowed, 3) the existence of a quantifier prefix such that the class of formulas with this prefix has exponential lower bound of time complexity. Some other theories are considered, too. The proofs are based on reduction of finite versions of the domino problems.