{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:00:23Z","timestamp":1760061623238,"version":"3.41.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,12]]},"DOI":"10.1023\/a:1006031329384","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:38:24Z","timestamp":1040517504000},"page":"357-380","source":"Crossref","is-referenced-by-count":50,"title":["A New Approach for Automatic Theorem Proving in Real Geometry"],"prefix":"10.1007","volume":"21","author":[{"given":"Andreas","family":"Dolzmann","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Sturm","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Weispfenning","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Abdallah, C. T., Dorato, P., Liska, R., Steinberg, S., and Yang, W.: Applications of quantifier elimination theory to control system design, in 4th IEEE Mediterranean Symposium on Control and Automation, IEEE, 1996.","key":"181213_CR1"},{"issue":"1\u20132","key":"181213_CR2","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/S0747-7171(88)80016-6","volume":"5","author":"D. S. Arnon","year":"1988","unstructured":"Arnon, D. S.: A bibliography of quantifier elimination for real closed fields, J. Symbolic Comput.\n5(1\u20132) (1988), 267\u2013274.","journal-title":"J. Symbolic Comput."},{"doi-asserted-by":"crossref","unstructured":"Basu, S., Pollack, R., and Roy, M.-R.: On the combinatorial and algebraic complexity of quantifier elimination, in S. Goldwasser (ed.), Proceedings of the 35th Annual Symposium on Foundations of Computer Science, Los Alamitos, CA, USA, November 1994, IEEE Computer Society Press, 1994, pp. 632\u2013641.","key":"181213_CR3","DOI":"10.1109\/SFCS.1994.365728"},{"key":"181213_CR4","volume-title":"Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal","author":"B. Buchberger","year":"1965","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal, Doctoral dissertation, Mathematical Institute, University of Innsbruck, Innsbruck, Austria, 1965."},{"doi-asserted-by":"crossref","unstructured":"Buchberger, B.: Applications of Gr\u00f6bner bases in non-linear computational geometry, in R. Jan\u03b2en (ed.), Trends in Computer Algebra, Proceedings, Lecture Notes in Comput. Sci. 296, Springer, 1988, pp. 52\u201380.","key":"181213_CR5","DOI":"10.1007\/3-540-18928-9_5"},{"key":"181213_CR6","volume-title":"A procedure to prove geometrical statements","author":"G. Carr\u00e1-Ferro","year":"1987","unstructured":"Carr\u00e1-Ferro, G. and Gallo, G.: A procedure to prove geometrical statements, Technical report, Dip. Mathematica Univ. Catania, Italy, 1987."},{"key":"181213_CR7","volume-title":"Mechanical Geometry Theorem Proving, Mathematics and Its Applications","author":"S.-C. Chou","year":"1988","unstructured":"Chou, S.-C.: Mechanical Geometry Theorem Proving, Mathematics and Its Applications, D. Reidel Publishing Company, Dordrecht, Boston, Lancaster, Tokyo, 1988."},{"issue":"3","key":"181213_CR8","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. E. Collins","year":"1991","unstructured":"Collins, G. E. and Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination, J. Symbolic Comput.\n12(3) (1991), 299\u2013328.","journal-title":"J. Symbolic Comput."},{"issue":"7","key":"181213_CR9","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/79204.79210","volume":"33","author":"A. Colmerauer","year":"1990","unstructured":"Colmerauer, A.: Prolog III, Communications of the ACM\n33(7) (1990), 70\u201390.","journal-title":"Communications of the ACM"},{"issue":"3","key":"181213_CR10","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/141897.141901","volume":"26","author":"R. M. Corless","year":"1992","unstructured":"Corless, R. M. and Jeffrey, D. J.: Well... it isn't quite that simple, ACM SIGSAM Bulletin\n26(3) (1992), 2\u20136. Feature.","journal-title":"ACM SIGSAM Bulletin"},{"unstructured":"Dolzmann, A. and Sturm, T.: Redlog user manual, Technical Report MIP-9616, FMI, Universit\u00e4t Passau, D-94030 Passau, Germany, October 1996. Edition 1.0 for Version 1.0.","key":"181213_CR11"},{"key":"181213_CR12","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1145\/258726.258851","volume-title":"Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (ISSAC 97)","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A. and Sturm, T.: Guarded expressions in practice, in W. W. K\u00fcchlin (ed.), Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (ISSAC 97), ACM Press, New York, 1997, pp. 376\u2013383."},{"issue":"2","key":"181213_CR13","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A. and Sturm, T.: Redlog: Computer algebra meets computer logic, ACM SIGSAM Bulletin\n31(2) (1997), 2\u20139.","journal-title":"ACM SIGSAM Bulletin"},{"issue":"2","key":"181213_CR14","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1006\/jsco.1997.0123","volume":"24","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A. and Sturm, T.: Simplification of quantifier-free formulae over ordered fields, J. Symbolic Comput.\n24(2) (1997), 209\u2013231.","journal-title":"J. Symbolic Comput."},{"unstructured":"Hong, H., Collins, G. E., Johnson, J. R., and Encarnacion, M. J.: QEPCAD interactive version 12. Kindly communicated to us by Hoon Hong, September 1993.","key":"181213_CR15"},{"issue":"2","key":"181213_CR16","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/jsco.1997.0121","volume":"24","author":"H. Hong","year":"1997","unstructured":"Hong, H., Liska, R., and Steinberg, S.: Testing stability by quantifier elimination, J. Symbolic Comput.\n24(2) (1997), 161\u2013187. Special issue on applications of quantifier elimination.","journal-title":"J. Symbolic Comput."},{"issue":"4","key":"181213_CR17","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1016\/S0747-7171(86)80007-4","volume":"2","author":"D. Kapur","year":"1986","unstructured":"Kapur, D.: Using Gr\u00f6bner bases to reason about geometry problems, J. Symbolic Comput.\n2(4) (1986), 399\u2013408.","journal-title":"J. Symbolic Comput."},{"unstructured":"Kutzler, B. A.: Algebraic Approaches to Automated Theorem Proving, PhD Thesis, Johannes Kepler Universit\u00e4t Linz, 1988. RISC-Linz series no. 88-74.0.","key":"181213_CR18"},{"issue":"4","key":"181213_CR19","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/S0747-7171(86)80006-2","volume":"2","author":"B. A. Kutzler","year":"1986","unstructured":"Kutzler, B. A. and Stifter, S.: On the application of Buchberger's algorithm to automated geometry theorem proving, J. Symbolic Comput.\n2(4) (1986), 389\u2013397.","journal-title":"J. Symbolic Comput."},{"issue":"5","key":"181213_CR20","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R. and Weispfenning, V.: Applying linear quantifier elimination, Comput. J.\n36(5) (1993), 450\u2013462. Special issue on computational quantifier elimination.","journal-title":"Comput. J."},{"key":"181213_CR21","doi-asserted-by":"crossref","first-page":"236","DOI":"10.2307\/2371070","volume":"58","author":"S. MacLane","year":"1936","unstructured":"MacLane, S.: Some interpretations of abstract linear dependence in terms of projective geometry, Amer. J. Math.\n58 (1936), 236\u2013240.","journal-title":"Amer. J. Math."},{"key":"181213_CR22","series-title":"Lecture Notes in Artif. Intell.","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/3-540-58156-1_28","volume-title":"Automated Deduction \u2013 CADE-12","author":"N. F. McPhee","year":"1994","unstructured":"McPhee, N. F., Chou, S.-C., and Gao, X.-S.: Mechanically proving geometry theorems using a combination of Wu's method and Collins' method, in Alan Bundy (ed.), Automated Deduction \u2013 CADE-12, Lecture Notes in Artif. Intell. 814, Springer, Berlin, Heidelberg, New York, 1994, pp. 401\u2013415."},{"key":"181213_CR23","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1098-6","volume-title":"Computational Geometry \u2013 An Introduction","author":"F. P. Preparata","year":"1985","unstructured":"Preparata, F. P. and Shamos, M. I.: Computational Geometry \u2013 An Introduction, Texts and Monographs in Computer Science, Springer, New York, 1985."},{"issue":"3","key":"181213_CR24","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J. Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, Part I\u2013III, J. Symbolic Comput.\n13(3) (1992), 255\u2013352.","journal-title":"J. Symbolic Comput."},{"key":"181213_CR25","first-page":"31","volume":"3","author":"A. Seidenberg","year":"1956","unstructured":"Seidenberg, A.: An elimination theory for differential algebra, Univ. California Publ. Math. (N.S.)\n3 (1956), 31\u201366.","journal-title":"Univ. California Publ. Math. (N.S.)"},{"key":"181213_CR26","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF01900296","volume":"7","author":"A. Seidenberg","year":"1956","unstructured":"Seidenberg, A.: Some remarks on Hilbert's Nullstellensatz, Arch. Math.\n7 (1956), 235\u2013240.","journal-title":"Arch. Math."},{"issue":"2","key":"181213_CR27","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1006\/jsco.1993.1035","volume":"16","author":"D.-M. Wang","year":"1993","unstructured":"Wang, D.-M.: An elimination method for polynomial systems, J. Symbolic Comput.\n16(2) (1993), 83\u2013114.","journal-title":"J. Symbolic Comput."},{"key":"181213_CR28","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-7091-6604-8_8","volume-title":"Automatic Practical Reasoning","author":"D.-M. Wang","year":"1995","unstructured":"Wang, D.-M.: Reasoning about geometric problems using an elimination method, in J. Pfalzgraf (ed.), Automatic Practical Reasoning, Springer-Verlag, Wien, 1995, pp. 147\u2013185."},{"key":"181213_CR29","volume-title":"Geometry theorems proved mechanically using Wu's method \u2013 part on Euclidean geometry","author":"D.-M. Wang","year":"1987","unstructured":"Wang, D.-M. and Gao, X.-S.: Geometry theorems proved mechanically using Wu's method \u2013 part on Euclidean geometry, Mathematics-Mechanization Research Preprints 2, Institute of Systems Science, Academia Sinica, Beijing, China, November 1987."},{"issue":"1","key":"181213_CR30","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields, J. Symbolic Comput.\n5(1) (1988), 3\u201327.","journal-title":"J. Symbolic Comput."},{"unstructured":"Weispfenning, V.: Parametric linear and quadratic optimization by elimination, Technical Report MIP-9404, FMI, Universit\u00e4t Passau, D-94030 Passau, Germany, April 1994. To appear in the J. Symbolic Comput.","key":"181213_CR31"},{"key":"181213_CR32","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/190347.190425","volume-title":"Proceedings of the International Symposium on Symbolic and Algebraic Computation in Oxford","author":"V. Weispfenning","year":"1994","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 the cubic case, in Proceedings of the International Symposium on Symbolic and Algebraic Computation in Oxford, ACM Press, New York, 1994, pp. 258\u2013263."},{"issue":"2","key":"181213_CR33","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 \u2013 the quadratic case and beyond, Appl. Algebra Eng. Comm. Comput.\n8(2) (1997), 85\u2013101.","journal-title":"Appl. Algebra Eng. Comm. Comput."},{"issue":"2","key":"181213_CR34","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1006\/jsco.1997.0122","volume":"24","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Simulation and optimization by quantifier elimination, J. Symbolic Comput.\n24(2) (1997), 189\u2013208. Special issue on applications of quantifier elimination.","journal-title":"J. Symbolic Comput."},{"key":"181213_CR35","series-title":"Lecture Notes in Comput. Sci.","first-page":"356","volume-title":"Symbolic and Algebraic Computation, Proceedings of ISSAC' 88","author":"F. Winkler","year":"1988","unstructured":"Winkler, F.: A geometrical decision algorithm based on the Gr\u00f6bner bases algorithm, in P. Gianni (ed.), Symbolic and Algebraic Computation, Proceedings of ISSAC' 88, Lecture Notes in Comput. Sci. 358, Springer, Berlin, Heidelberg, 1988, pp. 356\u2013363."},{"key":"181213_CR36","first-page":"159","volume":"21","author":"W.-T. Wu","year":"1978","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry, Scientia Sinica\n21 (1978), 159\u2013172, also Contemporary Mathematics\n29 (1984), 213\u2013234.","journal-title":"Scientia Sinica"},{"key":"181213_CR37","first-page":"207","volume":"4","author":"W.-T. Wu","year":"1984","unstructured":"Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometries, J. Systems Sci. Math. Sci.\n4 (1984), 207\u2013235.","journal-title":"J. Systems Sci. Math. Sci."},{"key":"181213_CR38","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1090\/conm\/029\/13","volume":"29","author":"W.-T. Wu","year":"1984","unstructured":"Wu, W.-T.: Some recent advances in mechanical theorem-proving of geometries, Contemporary Mathematics\n29 (1984), 235\u2013241.","journal-title":"Contemporary Mathematics"},{"key":"181213_CR39","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF02328446","volume":"2","author":"W.-T. Wu","year":"1986","unstructured":"Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometry, J. Automated Reasoning\n2 (1986), 219\u2013252.","journal-title":"J. Automated Reasoning"},{"key":"181213_CR40","volume-title":"On problems involving inequalities","author":"W.-T. Wu","year":"1992","unstructured":"Wu, W.-T.: On problems involving inequalities, Mathematics-Mechanization Research Preprints 7, Institute of Systems Science, Academia Sinica, Beijing, China, March 1992."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006031329384.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006031329384\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006031329384.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:36:54Z","timestamp":1749123414000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006031329384"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,12]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,12]]}},"alternative-id":["181213"],"URL":"https:\/\/doi.org\/10.1023\/a:1006031329384","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,12]]}}}