{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:36:06Z","timestamp":1694633766057},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. & Technol."],"published-print":{"date-parts":[[1999,9]]},"DOI":"10.1007\/bf02948789","type":"journal-article","created":{"date-parts":[[2008,9,12]],"date-time":"2008-09-12T23:52:03Z","timestamp":1221263523000},"page":"481-486","source":"Crossref","is-referenced-by-count":0,"title":["Fast theorem-proving and Wu\u2019s Method"],"prefix":"10.1007","volume":"14","author":[{"given":"Lian","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jimin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02948789_CR1","doi-asserted-by":"crossref","unstructured":"Tarski A. A Decision Method for Elementary Algebra and Geometry. 2nd ed. Univ. California Press, 1951.","DOI":"10.1525\/9780520348097"},{"key":"BF02948789_CR2","series-title":"Contemporary Mathematics","first-page":"1","volume-title":"Automated Theorem Proving: After 25 Years","author":"D Loveland","year":"1983","unstructured":"Loveland D. Automated theorem-proving: A quarter-century review. InAutomated Theorem Proving: After 25 Years, Bledsoe W (ed.), Contemporary Mathematics 29, 1983. American Mathematical Society, Providence, Rhode Island, pp. 1\u201346."},{"key":"BF02948789_CR3","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The computational complexity of logical theories","author":"J Ferrante","year":"1979","unstructured":"Ferrante J, Rackoff C W. The computational complexity of logical theories. Lecture Notes in Mathematics, 718, 1979, Springer-Verlag, New York."},{"key":"BF02948789_CR4","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"E Mayr","year":"1982","unstructured":"Mayr E, Meyer A. The complexity of the word problems for commutative semigroups and polynomials ideals.Advance in Mathematics, 1982, 46: 305\u2013329.","journal-title":"Advance in Mathematics"},{"key":"BF02948789_CR5","volume-title":"Basic Principles of Mechanical Theorem Proving in Geometries (part on Elementary Geometries)","author":"W T Wu","year":"1984","unstructured":"Wu W T. Basic Principles of Mechanical Theorem Proving in Geometries (part on Elementary Geometries), Beijing: Science Press, 1984 (in Chinese)."},{"key":"BF02948789_CR6","unstructured":"Gao X, Lin D. Wu\u2019s Method and Its Application. InMathematical Models, Ye Q (ed), Human Science and Technique Press, 1998."},{"key":"BF02948789_CR7","doi-asserted-by":"crossref","unstructured":"Buchberger B. Groebner Bases: An Algorithmic Method in Polynomial Ideal Theory. In Bose K (ed.)Multidimenstional Systems Theory, D. Reidel Publishing Co., 1985, pp. 184\u2013232.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"BF02948789_CR8","doi-asserted-by":"crossref","unstructured":"Collins G. Quantifier elimination for real closed fields by cylindrical algebraic decompisition. InProc. 2nd GI Conf., pp. 134\u2013183.","DOI":"10.1007\/3-540-07407-4_17"},{"key":"BF02948789_CR9","doi-asserted-by":"crossref","unstructured":"Loos R, Weispfenning V. Applying linear quantifiers elimination.The Computer Journal, 1993, 36(5): 450\u2013462, Special Issue on Computational Quantifier Elimination.","DOI":"10.1093\/comjnl\/36.5.450"},{"issue":"2","key":"BF02948789_CR10","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning V. Quantifier elimination for real algebra-the quadratic case and beyond.AAECC, 1997, 8(2): 85\u2013101.","journal-title":"AAECC"},{"key":"BF02948789_CR11","unstructured":"Yang L, Zhang J, Hou X. The System of Nonlinear Algebraic Equations and Mechanical Theorem-Proving. Shanghai Science and Education Press, 1996."},{"key":"BF02948789_CR12","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0747-7171(08)80069-7","volume":"10","author":"C Yap","year":"1990","unstructured":"Yap, C. Symbolic treatment of geometric degeneracies.J. Sym. Comp., 1990, 10: 349\u2013370.","journal-title":"J. Sym. Comp."},{"key":"BF02948789_CR13","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1090\/S0002-9947-1974-0349648-2","volume":"197","author":"A Seidernberg","year":"1974","unstructured":"Seidernberg A. Constructions in algebra.Trans. Am. Math. Soc., 1974, 197: 273\u2013313.","journal-title":"Trans. Am. Math. Soc."},{"key":"BF02948789_CR14","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/S0747-7171(89)80060-4","volume":"8","author":"H Kobayashi","year":"1989","unstructured":"Kobayashi H, Moritsugu S, Hogan R. On radical zero-dimension ideals.J. Symbolic Computation, 1989, 8: 545\u2013552.","journal-title":"J. Symbolic Computation"},{"key":"BF02948789_CR15","series-title":"Technical report","volume-title":"On the parameterization of algebraic curves","author":"X Gao","year":"1991","unstructured":"Gao X, Chou S. On the parameterization of algebraic curves. Technical report, Department of Computer Science, The University of Texas, Austin Texas, 1991."},{"key":"BF02948789_CR16","unstructured":"Gallo G, Mishra B. The complexity of resolvent resolved. InProceedings of the Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, 1994, pp. 280\u2013289."},{"key":"BF02948789_CR17","unstructured":"van der Waerden B. Abstract Algebra. Prinston Press, 1963."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02948789.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02948789\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02948789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T11:48:14Z","timestamp":1631792894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02948789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,9]]},"references-count":17,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1999,9]]}},"alternative-id":["BF02948789"],"URL":"https:\/\/doi.org\/10.1007\/bf02948789","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,9]]}}}