I implemented a Maple function CylindricalAlgebraicDecompose for computing cylindrical algebraic decompositions of semi-algebraic sets and a Maple function QuantifierElimination for doing real quantifier eliminations. The two functions are currently available in the RegularChains library.

The RegularChains library. Download

More information about this library can be found at www.regularchains.org.