Algorithms for sentences over integral domains (Q920964)

Arithmetical sentences are constructed from quantifiers, equality, logical connectives, constant symbols 0 and 1, and function symbols \(+\) and \(\cdot\) (multiplication). An integral domain is an associative- commutative ring with unit and without zero divisors. The paper contains two results on decidability of arithmetical \(\forall \exists\)-sentences over integral domains. Theorem 1. There exists a polynomial time algorithm deciding whether or not an arbitrary arithmetical \(\forall \exists\)-sentence in disjunctive or conjunctive normal form is valid in every integral domain of characteristic 0. Theorem 2. The \(\forall \exists\)-theory of integral domains is decidable. (The author does not know the complexity of the corresponding algorithm).