×

Complexity of deciding Tarski algebra. (English) Zbl 0689.03021

Let (*) \(\exists x_{1,1}...\exists x_{1,s_ 1}\forall x_{2,1}...\forall x_{2,s_ 2}...\exists x_{a,1}...\exists x_{a,s_ a}(P)\) be a formula of Tarski algebra, where P is a quantifier-free formula with atomic subformulas \((f_ i\geq 0)\), \(f_ i\in {\mathbb{Z}}[X_{1,1},...,X_{a,s_ a}]\), \(n=s_ 1+...+s_ a\), degrees \(\deg (f_ i)\leq d\), and the absolute value of each integer coefficient of \(f_ i\) is supposed to be less than \(2^ M\), \(1\leq i\leq k\). The main purpose of the present paper is to prove the following theorem: One can design a decision algorithm for Tarski algebra which determines the truth value of a formula of the kind (*) within a time polynomial in \(M(kd)^{O(n)^{4a-2}}\).
Reviewer: M.Tetruashvili

MSC:

03D15 Complexity of computation (including implicit computational complexity)
03B25 Decidability of theories and sets of sentences
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, (Proc. 16 ACM Symp. Th. Comput. (1984)), 457-464
[2] Chistov, A. L.; Grigor’ev, D. Yu., Polynomial-time Factoring of Multivariable Polynomials over a Global Field, (Preprint LOMI E-5-82, Leningrad (1982)) · Zbl 0509.68029
[3] Chistov, A. L.; Grigor’ev, D. Yu., Subexponential-time Solving Systems of Algebraic Equations I, (Preprint LOMI E-9-83, Leningrad (1983)) · Zbl 0596.12021
[4] Chistov, A. L.; Grigor’ev, D. Yu., Subexponential-time Solving Systems of Algebraic Equations. II, (Preprint LOMI E-I0-83, Leningrad (1983)) · Zbl 0596.12021
[5] Chistov, A. L.; Grigor’ev, D. Yu., Complexity of quantifier elimination in the theory of algebraically closed fields, Springer Lec. Notes Comp. Sci, 176, 17-31 (1984) · Zbl 0562.03015
[6] Chistov, A. L., Polynomial-time factoring of polynomials and finding compounds of a variety within the subexponential time, (Notes of Sci. Seminars of Leningrad Department of Math. Steklov Inst., 137 (1984)), 124-188, (in Russian). (English transl. to appear in J. Soviet Math.) · Zbl 0561.12010
[7] Cohen, P., Decision procedures for real and p-adic fields, Commun. Pure Appl. Math, 22, 131-153 (1969) · Zbl 0167.01502
[8] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Brakhage, H., Automata Theory and Formal Languages 2nd GI Conf., Kaiserslautern, 33 (1975)), 134-183, Springer Lec. Notes Comp. Sec. · Zbl 0318.02051
[9] Fischer, M.; Rabin, M., Super-exponential complexity of Presburger arithmetic, (Complexity of Computations (SIAM-AMS Proc. 7) (1974)), 27-41 · Zbl 0319.68024
[10] Grigor’ev, D. Yu., Factoring multivariable polynomials aver a finite field and solving systems of algebraic equations, (Notes of Sci. Seminars of Leningrad Department of Math. Steklav Inst., 137 (1984)), 20-79, (English transl, to appear in J. Soviet Math.) · Zbl 0561.12011
[11] Grigor’ev, D. Yu., Complexity of deciding first-order theory of real closed fields, (Proc. All-Union Conf. Appl. Logic, Novosibirsk (1985)), 64-66, (in Russian) · Zbl 0441.13007
[12] Grigor’ev, D. Yu., Computational Complexity in Polynomial Algebra, (Proc. International Congress of Mathematicians, Berkeley, California (1987)) · Zbl 0667.68054
[13] Grigor’ev, D. Yu.; Vorobjov, N. N., Solving systems of polynomial inequalities in subexponential time (1987), (Submitted.) · Zbl 0662.12001
[14] Heindel, L. E., Integer arithmetic algorithms for polynomial real zero determination, J. Assoc. Comp. Mach, 18, 4, 533-548 (1971) · Zbl 0226.65039
[15] Heintz, J., Definability and fast quantifier elimination in algebraically closed fields, Theor. Comp. Sci, 24, 239-278 (1983) · Zbl 0546.03017
[16] Lang, S., Algebra (1965), Addison-Wesley: Addison-Wesley New York · Zbl 0193.34701
[17] Lazard, D., Résolution des systèmes d’équation algébriques, Theor. Comp. Sci, 15, 77-110 (1981) · Zbl 0459.68013
[18] Lenstra, A. K., Factoring multivariable polynomials over algebraic number fields, Springer Lec. Notes Comp. Sci, 176, 389-396 (1984) · Zbl 0568.12001
[19] Mayr, E. W.; Meyer, A. R., The complexity of the word problem for commutative semigroups and polynomial ideals, Adv. Math, 46, 305-329 (1982) · Zbl 0506.03007
[20] Milnor, J., On a Betti numbers of real varieties, Proc. Amer. Math. Soc, 15, 2, 275-280 (1964) · Zbl 0123.38302
[21] Monk, L., An glementary-recursive Decision Procedure for Th(R, +,·) (1974), Ph.D. Thesis, Berkeley
[22] Seidenberg, A., A new decision method for elementary algebra and geometry, Ann. Math, 60, 365-374 (1954) · Zbl 0056.01804
[23] Shafarevich, I. R., Basic Algebraic Geometry (1974), Springer-Verlag: Springer-Verlag Berlin · Zbl 0284.14001
[24] Tarski, A., A Decision Method Jbr Elementary Algebra and Geometry (1951), University of California Press · Zbl 0044.25102
[25] Vorobjov, N. N.; Grigor’ev, D. Yu., Finding real solutions of systems of algebraic inequalities in subexponential time, Soviet Math. Dokl., 32, 1, 316-320 (1985) · Zbl 0607.65027
[26] Wiithrich, H., Ein Entseheidungsverthhren für die Theorie der reel-abgesehlossenen Körper, In Komplexität von Entscheidungs-Problemen. (Speeker E., Strassen V., Eds). Springer Lec. Notes Comp. Sci, 43, 138-162 (1976) · Zbl 0363.02052
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.