Simple Solution Formula Construction in Cylindrical Algebraic Decomposition Based Quantifier Elimination

Since Tarski (1951) gave the first quantifier elimination algorithm for real closed fields, various improvements and new methods have been devised and analyzed (Arnon 1981, 1988b; Ben-Or et al. 1986; Böge 1980; Buchberger and Hong 1991; Canny 1988; Cohen 1969; Collins 1975; Collins and Hong 1991; Fitchas et al. 1990a; Grigor’ev 1988; Grigor’ev and Vorobjov 1988; Heintz et al. 1989a; Holthusen 1974; Hong 1989, 1990a, 1990b, 1991a, 1991b, 1991c; Johnson 1991; Langemyr 1990; Lazard 1990; McCallum 1984; Renegar 1992a, 1992b, 1992c; Seidenberg 1954).