powerful tool for generically solving a wide range of problems based on logical
specifications. In contrast to general first-order provers, quantifier
elimination procedures are based on a fixed set of admissible logical symbols
with an implicitly fixed semantics. This admits the use of sub-algorithms from
symbolic computation. We are going to focus on real quantifier elimination and
its applications giving examples from geometry and verification. Beyond
quantifier elimination we are going to sketch work-in-progress on an incomplete
decision procedure for the existential fragment of the reals, which has been
successfully applied to the analysis of chemical reaction systems. We conclude
with an overview on quantifier-eliminable theories that have been realized in
our open-source computer logic software Redlog (www.redlog.eu).