Ehrenfeucht–Fraïssé goes automatic for real addition

AbstractThe decision problem of various logical theories can be decided by automata-theoretic methods. Notable examples are Presburger arithmetic FO(Z,+,<) and the linear arithmetic over the reals FO(R,+,<). Despite the practical use of automata to solve the decision problem of such logical theories, many research questions are still only partly answered in this area. One of these questions is the complexity of the automata-based decision procedures and the related question about the minimal size of the automata of the languages that can be described by formulas in the respective logic. In this article, we establish a double exponential upper bound on the automata size for FO(R,+,<) and an exponential upper bound for the first-order theory of the discrete order over the integers FO(Z,<). The proofs of these upper bounds are based on Ehrenfeucht–Fraïssé games. The application of this mathematical tool has a similar flavor as in computational complexity theory, where it can often be used to establish tight upper bounds of the decision problem for logical theories