Complex quantifier elimination in HOL

Abstract. Building on a simple construction of the complex numbers and a proof of the Fundamental Theorem of Algebra, we implement, as a HOL derived in-ference rule, a decision method for the first order algebraic theory of C based on quantifier elimination. Although capable of solving some mildly interesting problems, we also implement a more efficient semidecision procedure for the universal fragment based on Gröbner bases. This is applied to examples includ-ing the automatic proof of some simple geometry theorems. The general and universal procedures present an interesting contrast in that the latter can exploit the finding-checking separation to achieve greater efficiency, though this feature is only partly exploited in the present implementation.