Automatic theorem proving in field theory using quantifier elimination


Aleksandar Jovanović, Žarko Mijajlović




In this paper we describe a new method of elimination of quantifiers for the theories of algebraically closed fields and theory of ordered real closed fields which may be used for the theorem provers for these theories. The method is based on the properties of resultants of polynomials.