Quantifier Elimination in ACF and RCF

In this paper we will explain some basic notions related to quantifier elimination in the first order theories. We will give a general algorithm for quantifier elimination for any theory. The examples of theories which admit QE are theory of dense linear order (DLO), theory of algebraically closed fields (ACF) and theory of real closed fields (RCF). At the end, we will show the applications of quantifier elimination in ACF and RCF. The interesting applications can be seen in geometry, biology and control theory.