Ehrenfeucht-Fraissé Goes Automatic for Real Addition

Abstract

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,+,<)$, for which
   effective decision procedures can be built using automata.  Despite
   the practical use of automata to decide logical theories, many
   research questions are still only partly answered in this area.
   One of these questions is the complexity of such 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 paper, we establish a double exponential
   upper bound on the automata size for FO$(R,+,<)$ and an exponential
   upper bound for the discrete order over the integers FO$(Z,<)$.
   The proofs of these upper bounds are based on
   Ehrenfeucht-Fraiss{'\e} 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.