zbMATH — the first resource for mathematics

A bibliography of quantifier elimination for real closed fields. (English) Zbl 0646.03024
A list of papers on quantifier elimination for real closed fields are referred with comments on their destination (e.g. tutorial, research etc.). It seems to be complete, but unfortunately short summaries and comparisons of different algorithms fail, what yields difficulties for the novice in this area. Also it is regretable that the supporting algorithms such as polynomial factoring and solving systems of algebraic equations tightly connected with the subject under discussion are absent.
Reviewer: D.Yu.Grigor’ev

03C10 Quantifier elimination, model completeness and related topics
12L12 Model theory of fields
68W30 Symbolic computation and algebraic computation
00A15 Bibliographies for mathematics in general
Full Text: DOI
[1] A’Compo, N., Sur la premiére portia du seiziéme problém de Hilbert. Séminalre bourbaki, Springer lec. notes math., 770, 207-227, (1979), (HilbertSixteenthProblem)
[2] Arnborg, S.; Fang, H.-C., Algebraic decomposition of regular curves, J. symb. comp., 5, (1988), (this issue). (ComplexityResult, ResearchResult)
[3] Arnol’d, V.I.; Oleinik, O.A., Topology of real algebraic manifolds, Vestnik moskovskogo univ. matematika (Moscow university mathematics bulletin), 34, 7-17, (1979), (RealAlgebraicGeometry) · Zbl 0423.14013
[4] Arnon, D.S., A cellular decomposition algorithm for semi-algebraic sets, Proceedings of an International Symposium on Symbolic and Algcbraic Manipulation (EUROSAM ’79), Springer lec. notes comp. sci., 72, 301-315, (1979), (CollinsAlgorithm, Exposition; CcllAdjacencyAlgorithm, CollinsAlgorithm, ResearchResult)
[5] Arnon, D.S., Algorithms for the geometry of semi algebraic sets, (1981), Comp. Sci. Dept., Univ. Wisconsin-Madlson, (CollinsAlgorithm, Exposition: CellAdjacencyAlgorithm, ClusteringAlgorithm, CollinsAlgorithm, ResearchResult, Implementation, Examples)
[6] Arnon, D.S.; MeCallum, S., Cylindrical algebraic decomposition by quantifier elimination, Proceedings of the European Computer Algebra Conference (EUROCAM ’82), Springer lec. notes comp. sci., 144, 215-222, (1982), (CollinsAlgorithm, ResearchResult, Examples)
[7] Arnon, D.S., Topologically reliable display of algebraic curves, (), 219-227, (CurveDisplay, Implementation, CollinsAlgorithm)
[8] Arnon, D.S.; Collins, G.E.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, Slam .J. comp., 13, 4, 865-877, (1984), (CollinsAlgorithm, Exposition, Implementation, Examples) · Zbl 0562.14001
[9] Arnon, D.S.; Collins, G.E.; McCallum, S., Cylindrical algebraic decomposltion II: an adjacency algorithm for the plane, SIAM J. comp., 13, 4, 878-889, (1984), (CellAdjacencyAlgorithm, CollinsAlgorithm, ResearchResult, Implementation, Examples) · Zbl 0562.14001
[10] Arnon, D.S., A cluster-based cylindrical algebraic decomposition algorithm, J. symb. comp., 5, (1988), (this issue). (CellAdjacencyAlgorithm, ClusteringAlgorithm, CollinsAlgorithm, ResearchResult) · Zbl 0648.68056
[11] Arnon, D.S., Geometric reasoning with logic and algebra, Artificial intelligence J., (1988), (special issue on Geometric Reasoning and Artificial Intelligence; to appear). (Exposition, GeometryTheoremProving, RootClassification, CollinsAlgorithm, Implementatlon, Examples, ResearchResult) · Zbl 0705.68086
[12] Arnon, D.S.; MeCallum, S., A polynomial-time algorithm for the topological type of a real algebraic curve, J. symb. comp., 5, (1988), (this issue). (CellAdjacencyAlgorithm, CollinsAlgorithm, HilbertSixteenthProblem, ResearchResult, Implementation, Examples)
[13] Arnon, D.S.; Mignotte, M., On mechanical quantifier ellmination for elementary algebra and geometry, J. symb. comp., 5, (1988), (this issue). (RealClosedFields, Examples, CollinsAlgorithm, Implementation, ResearchResult) · Zbl 0644.68051
[14] Arnon, D.S.; Collins, G.E.; McCallum, S., An adjacency algorithm for cylindrical algebraic decompositions of three dimensional space, J. symb. comp., 51, (1988), (this issue). (CellAdjacencyAlgorithm, CollinsAlgorithm, ResearchResult, Examples) · Zbl 0648.68055
[15] Bajaj, C., Compliant motion planning wlth geometric models, Proc. third ACM symp. computational geometry, 171-180, (1987), (ResearchResult, MotionPlanning)
[16] Becker, E., On the real spectrum of a ring and its application to semialgebraic geometry, Bull. (new series) American math. soc., 15, 19-60, (1986), (RealAlgebraicGeometry, Tutorial, ResearchResult) · Zbl 0634.14016
[17] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, J. comp. sys. sci., 32, 251-264, (1986), (Ben-Or/Kozen/ReifAlgorithm, ComplexityResult, ResearchResult) · Zbl 0634.03031
[18] Berman, L., The complexity of loglcal theories, Theor. comp. sci., 11, 71-77, (1980), (ComplexityResult RescarchResult)
[19] Bochnak, J.; Coste, M.; Roy, M.F., Geometrie algébrique Réelle, (1987), Sprlnger-Verlag Berlin, (Ergebnisse der Mathematik) (RealAlgebraicGeometry, Exposition, ResearchResult)
[20] Böge, W., Quantifier elimination for real closed fields, Proc. AAECC-3. Springer lec. notes comp, sci., (1986) · Zbl 0622.03021
[21] Brumfiel, G., Partially ordered rings and semi-algebraic geometry, (), (RealAlgebraicGeometry, Tutorial, ResearchResult ; CohenAlgorithm, Exposition) · Zbl 0415.13015
[22] Buchberger, B.; Loos, R.; Collins, G.E., (), (Survey, Tutorial, Exposition)
[23] Canny, J., The complexity of robot motion planning, (1987), Dept. of Electr. Engin & Comp. Sci., Massachusetts Inst. of Tech., (ResearchResult, ComplexityResult, MotionPlanning, RealClosedFields)
[24] Canny, J., A new algebraic method for robot motion planning and real geometry, Proc. 1987 IEEE conf. on foundations of comp. sci. (FOCS), (1987), (ResearchResult, ComplexityResult, MotlonPlannlng, RealClosedFields)
[25] Chazelle, B., Fast searching in a real algebraic manifold with applications to geometric complexity, Proc. CAAP ’85. sprinper Lee. notes comp. sci., (1985), (GeometricSearching, ResearchResult, Survey; CollinsAlgorithm, Exposition) · Zbl 0605.68054
[26] Chou, Y.S., Proving elementary geometry theorems using Wu’s method, (), 243-286, (GeometryTheoremProving)
[27] Chou, Y.S., Mechanical geometry theorem proving, (1988), D. Reidel New York, (GeometryTheoremProving) · Zbl 0661.14037
[28] Cohen, P.J., Decision procedures for real and padic fields, Comm. pure appl. math, 22, 131-151, (1969), (CohenAlgorithm ResearchResult)
[29] Collins, G.E., The Tarski decision procedure, Proc. ACM natl. conf., (1956), (TarskiAlgorithm, Exposition)
[30] Collins, G.E., Tarski’s decision method for elementary algebra, (), 64-70, (TarskiAlgorithm, Exposition) · Zbl 0201.33102
[31] Collins, G.E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the Second GI Conference on Automata Theory and Formal Languages, Springer lec. notes comp. sci., 33, 515-532, (1975), (CollinsAlgorithm, ResearchResult)
[32] Collins, G.E., Quantifier elimlnatlon for real closed fields by cylindrical algebraic decomposition - a synopsis, ACM SIGSAM bull., 10, 1, 10-12, (1976), (CollinsAlgorithm, Exposition)
[33] Collins, G.E., Factorization in cylindrical algebraic decomposition, Proceedings of the Euro- pean Computer Algebra Conference (EUROCAM ’82), Springer lec. notes comp. sci., 144, 212-214, (1982), (CollinsAlgorithm, ResearchResult)
[34] Collins, G.E., Quantifier elimination for real closed fields: a guide to the literature, (), 79-81, (RealClosedFields, CollinsAlgorithm, Survey) · Zbl 0495.03016
[35] Coste, M.; Roy, M.F., Thom’s lemma, the coding of reai algebraic numbers and the computation of the topology of semi-algebraic sets, J. symb. comp., 5, (1988), (this issue). (RealAlgebraicGe- ometry, CellAdjacencyAlgorithm, ResearchResult) · Zbl 0689.14006
[36] Davenport, J., Computer algebra for cylindrical algebraic decomposition, (1985), Royal Inst. of Tech., Dept. of Numerical Analysis and Computer Science Stockholm, Sweden, (CollinsAlgorithm, Survey)
[37] Davenport, J., A piano movers problem, ACM SIGSAM bull., 20, 70, 15-17, (1986), (MotionPlanning) · Zbl 0623.68036
[38] Davenport, J.; Siret, Y.; Tournier, E., Calcul formal: systémes et algorithmes de manipulation, algébriques, (1987), Masson Paris, (Exposition)
[39] Davenport, J.; Heintz, J., Real quantifier elimination is doubly exponential, J. symb. comp., 5, (1988), (this issue). (ComplexityResult, ResearchResult) · Zbl 0663.03015
[40] Delzell, C., A finiteness theorem for open semi-algebraic sets, with applications to Hilbert’s 17th problem, (), 79-97, (RealAlgebraicGeometry, ResearchResult) · Zbl 0495.14013
[41] Delzell, C., A continuous, constructive solution to Hilbert’s 17th problem, Invent. math., 76, 365-384, (1984), (RealAlgebraicGeometry, ResearchResult) · Zbl 0547.12017
[42] Dershowitz, N., A note on simplification orderings, Info. proc. letters, 9, 5, 212-215, (1979), (GeneralApplications) · Zbl 0433.68044
[43] Diekmann, M.A., Applications of model theory to real algebraic geometry: a survey. methods in mathematical logic Proceedings 1983, Springer lec. notes math., 1130, 76-150, (1985), (RealAlgebraicGeometry, Survey)
[44] Dubois, D.W., A nullstellensatz for ordered fields, Ark. math., 8, 111-114, (1969), (RealAlgebraic- Geometry, ResearchResult) · Zbl 0205.06102
[45] Dubois, D.W.; Efroymson, G., Algebraic theory of real varieties, (), 107-135, (RealalgebraicGeometry, ResearchResult, Exposition) · Zbl 0216.05401
[46] (), (RealAlgebraicGeometry, ResesrchResult, Exposition)
[47] (), (RealAlgebraicGeometry, ResearchResult, Exposition)
[48] Ferrante, J.; Rackoff, C., A decision procedure for the first order theory of real addition with order, SIAM J. comp., 4, 69-76, (1978), (ComplexityResult, ResearchResult) · Zbl 0294.02022
[49] Ferrante, J.; Rackoff, C., The complexity of decision procedures for logical theories, Springer lec. notes math., 718, (1979), (ComplexityResult, ResearchResult, Exposition)
[50] Fischer, M.; Rabin, M., Super-exponentlal complexity of Presburger arithmetic, (), 27-41, (ComplexityResult, ResearchResult)
[51] Fitchas, N.; Galligo, A.; Morgenstern, J., Algorithmes rapides en sequentiel et en parallele pour l’elimination de quantificateurs en geometrique elementaire, Seminaire structures algebriques ordonnees, (1987), UER de Mathematiques, Univ. Paris VII. (to appear) (ComplexityResult, Research.Result)
[52] Galligo, A.; Heintz, J.; Morgenstern, J., Parallelism and fast quautifier elimination over algebraically (and real) closed fields, Proceedings of the FCT 187 Conf, Kazan USSR, Springer lec. notes comp. sci., (1987), (ComplexityResult, ResearchResult)
[53] Grigor’ev, D.Y., The complexity of deciding Tarski algebra, J. symb. comp., 5, (1988), (this issue). (ComplexityResult, ResearchResult) · Zbl 0689.03021
[54] Grigor’ev, D.Y.; Vorobjov, N.N., Solving systems of polynomial inequalities in subexponential time, J. symb. comp., 5, (1988), (this issue). (ComplexityResult, ResearchResult) · Zbl 0662.12001
[55] Gudkov, D.A., The topology of real projective algebraic varietles, Russian math. surveys, 29, 1-79, (1974), (RealAlgebraicGeometry, Survey) · Zbl 0316.14018
[56] Heintz, J.; Wüthrich, H., An efficient quantifier elimination procedure for algebraically closed fields, ACM SIGSAM bull., 9, 11, (1975), (ComplexityResult, ResearchResult)
[57] Heintz, J., Definability and fast quantifier elimination in algebraically closed fields, Theoretical comput. sci., 24, 239-277, (1983), (ComplexityResult, ResearchResult) · Zbl 0546.03017
[58] Hironaka, H., Triangulations of algebraic sets, AMS syrup. in pure math, 29, 165-185, (1975), (RealAlgebraicGeometry)
[59] Holthusen, C., Vereinfachungen für Tarski’s entacheidungsverfahren der elementaren reeleen algebra, (1974), Diplomarbeit, Univ. Heidelberg, (TarskiAlgorithm, ResearchResult)
[60] Jacobson, N., Lectures in abstract algebra, (1964), D. Van Nostrand Princeton, NJ, (TarskiAlgo- rithm, SeidenbergAlgorithm, Algebra, Tutorial)
[61] Jacobson, N., Basic algebra, (1974), W.H. Freeman San Francisco, CA, (TarskiAlgoritbm, Seiden-bergAlgorithm, Algebra, Tutorial, GeneralApplications) · Zbl 0284.16001
[62] Kahn, P.J., Counting types of rigid frameworks, Inventiones math., 55, 297-308, (1979), (GeneralApplications, CollinsAlgorithm) · Zbl 0427.51010
[63] Kaplansky, I., Hilbert’s problems- preliminary edition, Manuscript, math, (1977), Dept., Univ. Chicago, (HilbertSixteenthProblem, Exposition)
[64] Kapur, D., Geometry theorem proving using Hilbert’s nullstellensatz, (), 202-208, (Geometry- TheoremProving)
[65] Kaput, D., A refutational approach to geometry theorem proving, Artificial intelligence J, (1988), (special issue on geometric reasoning and artificial intelligeace; to appear). (GeometryTheorem- Proving)
[66] Kozen, D.; Yap, C.K., Algebraic cell decomposition in NC, Proc. IEEE conf. on foundations of comp. sci. (FOCS), 515-521, (1985), (CellDecompositionAlgorithm, CellAdjacencyAlgorithm, Ben- Or/Kozen/ReifAlgorithm, ResearchResult)
[67] Kreisel, G.; Krivine, J.L., Elements of mathematical logic (model theory), (1967), North-Holland Amsterdam, (RealClosedFields, Tutorial) · Zbl 0155.33801
[68] Kreisel, G., Some uses of proof theory for finding computer programs, Colloques interna- tioneauz du CNRS, 249, 123-134, (1975), (RealClosedFields, Examples)
[69] Kreisel, G., From foundations to science; justifying and unwinding proofs, (), 63-72, (RealClosedFields, Examples)
[70] Kutzler, B.; Stifter, S., (), 209-214, (GeometryTheoremProving)
[71] Lam, T.Y., Introduction to real algebra, Rocky mountain J. math., 14, 767-814, (1984), (Survey, Tutorial, Exposition, RealAlgebraicGeometry) · Zbl 0577.14016
[72] Lazard, D., Quantifier elimination: optimal solution for two classical examples, J. symb. comp., 5, (1988), (this issue). (RealClosedFields, Examples, ResearchResult) · Zbl 0647.03023
[73] MacIntyre, A.; McKenna, K.; van den Dries, L., Elimination of quantifiers in algebraic structures, Advances in math., 47, 74-87, (1983), (LoglcalTheorics) · Zbl 0531.03016
[74] Massey, W.S., Homology and cohomoloyy theory, (1978), Marcel Dekker New York, NY, (CellComplexes) · Zbl 0377.55005
[75] McCallum, S., Constructive triangulation of real curves and surfaces (msc thesis), (1979), Math. Dept., Univ. of Sydney Australia, (RealAlgebraicGcometry, CellAcljaccncyAlgorithm, ResearchResult)
[76] McCallum, S., An improved projection operator for cylindrical algebraic decompoaitlon (ph.D. thesis), (1985), Comp. Sci. Dept., Univ. Wisconsin-Madison, (CollinsAlgorithm, ResearchResult, Implementation)
[77] McCallum, S., An improved projection operation for cylindrical algebraic decompositlon of three-dlmenslonal space, J. symb. comp, 5, (1988), (this issue). (CollinsAlgorithm, ResearchResult, Implementation)
[78] Meserve, B., Decision methods for elementary algebra, Ameer. math. monthly, 62, 1-8, (1955), (TarskiAlgorithm, Tutorial) · Zbl 0064.00801
[79] Monk, L., An elementary recursive decision procedure for th(R_1+1*). manuscript, math, (1974), Dept., Univ. California Berkeley, (MonkAlgorithm, ResearchResult)
[80] Monk, L., Elementary recursive decision procedures (ph.D. thesis), (1975), Math. Dept., Univ. California Berkeley, (MonkAlgorithm, ResearchResult)
[81] Müller, F., Ein ezakter algorithmus zur nichtlinearen optimierung für beliebige polynome mit mehreren veranderlichen, (1978), Verlag Anton Hain Meisenheim am Glan, (GeneralApplications, Implementations, Examples, ResearchResult)
[82] Mundy, J.; Kapur, D., Wu’s method: an informal introduction, Artificial intelligence J., (1988), (special issue on geometric reasoning and artificial intelligence; to appear). (GeometryTheorem- Proving)
[83] O’Rourke, J., The complexity of computing minimum convex covers for polygons, (1982), Manscrpt, Dept. of Electr. Engin. and Comp. Sci Johns Hopkins Univ., (GeneralApplications)
[84] Paugam, A., Algorithmes d’elimination des quantificateurs, (1986), Manuscript, Math. Dept., Univ. Rennes, (SeidenbergAlgorithm, CollinsAlgorithm, Exposition) · Zbl 0594.03016
[85] Prestel, A., Lecture on formally real fields. Rio de Janeiro: IMPA 1975, Springer lec. notes math, 1093, (1984), (RealClosedFields)
[86] Prill, D., On approximation and incidence in cylindrical algebralc decompositions, SIAM J. comp., 15, 972-993, (1986), (CellAdjacencyAlgorithm, CollinsAlgorithm, ResearchResult, ComplexityResult) · Zbl 0643.14002
[87] Robin, M., Decidable theories, (), 595-630, (RealClosedFields, Tutorial)
[88] Risler, J.-J., Sur le 16 probléme de Hilbert: un résumé et quelques questions, (), 11-25, (HilbertSixteenthProblem, Survey)
[89] Risler, J.-J., Some aspects of complexity in real algebraic geometry, J. symb. comp., 5, (1988), (this issue). (RealAlgebraicGeometry Survey)
[90] Robinson, A., Introduction to model theory and the metamathematics of algebra, (1965), North-Holland Amsterdam, (RealClosedFields, Tutorial)
[91] Robinson, A., A decision method for elementary algebra and geometry - revisited, AMS syrup. in pure math., 25, 139-152, (1974), (TarskiAlgorithm, Survey)
[92] Schwartz, J.T.; Sharir, M., On the ‘piano movers’ problem H. general techniques for computing topological properties of real algebraic manifolds, Adv. applied math., 4, 298-351, (1983), (MotionPlanning, ResearchResult; CollinsAlgorithm, Exposition) · Zbl 0554.51008
[93] Schwartz, J.; Sharir, M., A survey of motion planning and related geometric algorithms, Artificial intelligence J., (1988), (special issue on Geometric Reasoning and Artificial Intelligence; to appear). (MotionPlanning, Survey) · Zbl 0676.68086
[94] Seidenberg, A., A new decision method for elementary algebra, Annals of math., 80, 365-374, (1954), (SeldenbergAlgorithm, ResearchResult) · Zbl 0056.01804
[95] Sharir, M.; Schorr, A., On shortest paths in polyhedral spaces, Proc. 16th ACM syrup. on theory of computing (STOC), 144-153, (1984), (GeneralApplications, GeometricSearching)
[96] Smorynski, C., Skolem’s solution to a problem of Frobenius, Math. inielligeneer, 3, 3, 123-132, (1981), (LogicalTheories, RealClosedFields, ComlnsAlgorithm, Tutorial, Examples,) · Zbl 0498.10013
[97] Sontag, E., Real addition and the polynomial hierarchy, Info. proc. letters, 20, 115-120, (1985), (ResearchResult, ComplexityResult,) · Zbl 0575.03030
[98] Struth, M., Vorzeichenbestimmung für polynome auf der zellenzerlegung nach collins, (1980), Diplomarbeit, Univ. Heidelberg, (CollinsAlgorithm, ResearchResult,)
[99] Tarski, A., A decision method for elementary algebra and geometry, (), (TarskiAlgorithm, Research.Result, Exposition, Examples) · Zbl 0044.25102
[100] Tarski, A., What is elementary geometry?, (), 16-29, (TarskiAlgorithm, GeometryTheoremProving)
[101] Thom, R., Structural stability and morphogenesis, (1972), Benjamin New York, (RealAlgebraicGeometry, ResearchResult, Exposition)
[102] van der Waerden, B.L.; Schütte, K., DoS problem der dreizehn kugeln, Math. ann., 125, 325-334, (1952), (RealClosedFields, ResearchResult, Examples) · Zbl 0050.16701
[103] van der Waerden, B.L., Algebra, (1970), Frederick Ungar New York, (RealClosedFields, Algebra, Exposition, Tutorial)
[104] Wang, H., Popular lectures on mathematical logic, (1981), Belling: Science Press. New York Van Nostrand Reihnold, (RealClosedFields, Tutorial)
[105] Weispfenning, V., The complexity of linear problems in fields, J. symb. comp., 5, (1988), (this issue). (ComplexityResult, ResearchResult) · Zbl 0646.03005
[106] Whitney, H., Elementary structure of real algebraic varieties, Ann. of math., 66, 545-556, (1957), (RealAlgebraicGeometry, ResearchResult) · Zbl 0078.13403
[107] Wilson, G., Hilhert’s sixteenth problem, Topolooy, 17, 53-73, (1978), (HilbertSixteenthProblem, Survey) · Zbl 0394.57001
[108] W.-T., Wu, Basic principles of mechanical theorem proving in elementary geometries, J. syst. sci. & math. sci., 4, 207-235, (1984), Reprinted in J. Automated Reasoning (1986), 2, 221-252. (GeometryTheoremProving)
[109] Wüthrich, H., Ein entscheidungsverfahren für die theorie der reell-abgeschlossenen Körper, Springer lec. notes comp. sci., 43, 138-162, (1976), (WuethrichAlgorithm, RcsearchResult) · Zbl 0363.02052
[110] Wüthrich, H., Ein schnelles quantoreneliminationsverfahren für die theorie der algebraisch abgeschlossenen Körper (ph.D. thesis), (1977), Philisophischen Fakultät II, Univ. Zurich, (ResearchResult)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.