A Decision Procedure for the First Order Theory of Real Addition with Order

Abstract

Consider the first order theory of the real numbers with the function + (plus) and the predicate $ < $ (less than). Let S be the set of true sentences of this theory. We first present an elimination of quantifiers decision procedure for S, and then analyze it to show that it takes at most time $2^{2cn} $, where c is a constant, to decide sentences of length n. We next show that a given sentence does not change in truth value when each of the quantifiers is limited to range over an appropriately chosen finite set of rationals. This fact leads to a new decision procedure for S which uses at most space $2^{cn} $. We also remark that our methods lead to a decision procedure for Presburger arithmetic which operates within space $2^{2cn} $. These upper bounds should be compared with the results of Fischer and Rabin [2] that for some constant c, real addition requires time $2^{cn} $ and Presburger arithmetic requires time $2^{2cn} $.