A class of mechanically decidable problems beyond Tarski’s model. (English) Zbl 1133.68423
Summary: By means of dimension-decreasing method and cell-decomposition, a practical algorithm is proposed to decide the positivity of a certain class of symmetric polynomials, the number of whose elements are variable. This is a class of mechanically decidable problems beyond Tarski’s model. To implement the algorithm, a program written in Maple is developed which can decide the positivity of these polynomials rapidly.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
Keywords:
symmetric polynomial inequality; cell-decomposition; Tarski’s sentence; Tarski’s model; mechanically decidable problemReferences:
| [1] | Tarski A. A Decision Method for Elementary Algebra and Geometry, 2nd ed. Berkeldy: University of California Press, 1951 · Zbl 0044.25102 |
| [2] | Wu W T. On the decision problem and the mechanization of theorem-proving in elementary geometry. Science in China, 21: 150–172 (1978) · Zbl 0376.68057 |
| [3] | Chou S C. Mechanical Geometry Theorem Proving. Dordrecht: Reidel, 1988 · Zbl 0661.14037 |
| [4] | Buchberger B. Grobner bases: An algorithmic method in polynomial ideal theory. In: Multidimensional Systems Theory. Dordrecht: Reidel, 1985, 184–232 · Zbl 0587.13009 |
| [5] | Kapur D. Geometry theorem proving using Hilbert’s Nullstellensata. In: Proc. SYMSAC’86. New York: ACM Press, 1986, 202–208 |
| [6] | Kutzler B, Stifter S. Automated geometry theorem proving using Buchberger’s algorithm. In: Proc SYM-SAC’86. New York: ACM Press, 1986, 209–214 · Zbl 0629.68086 |
| [7] | Yang L, Zhang J Z, Hou X R. Nonlinear Algebraic Equation System and Automated Theorem Proving. Shanghai: Shanghai Scientific and Technological Education Publishing House, 1996 |
| [8] | Zhang J Z, Yang L, Deng M K. The parallel numerical method of mechanical theorem proving. Theor Comput Sci, 74(3): 253–271 (1990) · Zbl 0701.68087 · doi:10.1016/0304-3975(90)90077-U |
| [9] | Chou S C, Gao X S, Zhang J Z. Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. Singapore: World Scientific, 1994 · Zbl 0941.68503 |
| [10] | Collins G E, Hong H. Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, 12: 299–328 (1991) · Zbl 0754.68063 · doi:10.1016/S0747-7171(08)80152-6 |
| [11] | Timofte V. On the positivity of symmetric polynomial functions I. J Math Anal Appl, 284: 174–190 (2003) · Zbl 1031.05130 · doi:10.1016/S0022-247X(03)00301-9 |
| [12] | Timofte V. On the positivity of symmetric polynomial functions, Part II: Lattice general results and positivity criteria for degrees 4 and 5. J Math Anal Appl, 284: 652–667 (2005) · Zbl 1058.05065 · doi:10.1016/j.jmaa.2004.09.055 |
| [13] | Choi M D, Lam T Y, Reznick B. Even symmetric sextics. Math Z, 195: 559–580 (1987) · Zbl 0654.10024 · doi:10.1007/BF01166704 |
| [14] | Yang L, Xia B C. Computational real algebraic geometry. In: Wang D M, ed. Selected Lectures in Symbolic Computation (in Chinese). Beijing: Tsinghua University Press, 2003 |
| [15] | Dolzman A, Sturm T. REDLOG: Computer algebra meets computer logic. Acm Sigsam Bulletin, 31(2): 2–9 (1997) · doi:10.1145/261320.261324 |
| [16] | Yang L, Hou X R, Xia B C. A complete algorithm for automated discovering of a class of inequality-type theorems. Sci China Ser F-Info, 44: 33–49 (2001) · Zbl 1125.68406 · doi:10.1007/BF02713938 |
| [17] | Yang L, Xia S H. Automated proving for a class of constructive geometric inequalities. Chinese Journal of Computers (in Chinese), 26(7): 769–778 (2003) |
| [18] | Yang L, Zhang J. A practical program of automated proving for a class of geometric inequalities, automated deduction in geometry. Lecture Notes in Artificial Intelligence 2061. Berlin Heidelberg: Springer-Verlag, 2001, 41–57 · Zbl 0985.68556 |
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.
