Algorithms for sentences over integral domains (Q920964)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Algorithms for sentences over integral domains |
scientific article |
Statements
Algorithms for sentences over integral domains (English)
0 references
1990
0 references
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).
0 references
decidability of arithmetical \(\forall \exists \)-sentences over integral domains
0 references
algorithm
0 references