10.4230/LIPICS.STACS.2008.1364
Klaedtke, Felix
Felix
Klaedtke
Ehrenfeucht-Fraissé Goes Automatic for Real Addition
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2008
Automata theory
automata-based decision procedures for logical theories
upper bounds
minimal sizes of automata
linear arithmetic over the reals
f
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
2008
2008-02-06
2008-02-06
2008-02-06
en
urn:nbn:de:0030-drops-13649
10.4230/LIPIcs.STACS.2008
978-3-939897-06-4
1868-8969
10.4230/LIPIcs.STACS.2008
LIPIcs, Volume 1, STACS 2008
25th International Symposium on Theoretical Aspects of Computer Science
2013
1
39
445
456
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Albers, Susanne
Susanne
Albers
Weil, Pascal
Pascal
Weil
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2008
1
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
195123 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 1, 25th International Symposium on Theoretical Aspects of Computer Science, pages 445-456