Mixed real-integer linear quantifier elimination
Volker Weispfenning · 1999
Consider the elementary theory T of the real numbers in the language L 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. We provide closely matching upper and lower bounds for the complexity of the quantifier elimination and decision problem for T. Applications include a characterisation of T-definable subsets of the real line, and the modeling of parametric mixed integer linear optimization, of continuous phenomena with periodicity, and the simulation and analysis of hybrid control systems. We also consider the elementary theory of reals in variations of this language in view of quantifi...