Consider the elementary theory T of the real numbers in the languageL having 0,1 as constants, addition and subtraction and integer part as operations, and equality, order and congruences modulo natural number constants as relations. We show that T admits an effective quantifier elimination procedure and is decidable. Moreover this procedure provides sample answers for existentially quantified variables. The procedure comprises as special cases linear elimination for the reals and for Presburger arithmetic of asymptotically optimal complexity. Applications include parametric mixed integer linear optimization and the simulation and analysis of hybrid control systems and of continuous phenomena with periodicity. We also consider the elementary theory of reals in variations of this language in view of quantifier elimination and decidability.
cetindag@fmi.uni-passau.de
Erika Cetindag, Martin Griebl