License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2008.1364
URN: urn:nbn:de:0030-drops-13649
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1364/
Go to the corresponding LIPIcs Volume Portal

Klaedtke, Felix

Ehrenfeucht-Fraissé Goes Automatic for Real Addition

pdf-format:
22011.KlaedtkeFelix.Paper.1364.pdf (0.2 MB)

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.

BibTeX - Entry

@InProceedings{klaedtke:LIPIcs:2008:1364,
  author =	{Felix Klaedtke},
  title =	{{Ehrenfeucht-Fraiss{\'e}  Goes Automatic for Real Addition}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{445--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Susanne Albers and Pascal Weil},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1364},
  URN =		{urn:nbn:de:0030-drops-13649},
  doi =		{10.4230/LIPIcs.STACS.2008.1364},
  annote =	{Keywords: Automata theory, automata-based decision procedures for logical theories, upper bounds, minimal sizes of automata, linear arithmetic over the reals, f}
}

Keywords: Automata theory, automata-based decision procedures for logical theories, upper bounds, minimal sizes of automata, linear arithmetic over the reals, f
Collection: 25th International Symposium on Theoretical Aspects of Computer Science
Issue Date: 2008
Date of publication: 06.02.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI