Ehrenfeucht-Fraissé Goes Automatic for Real Addition

Author Felix Klaedtke



PDF
Thumbnail PDF

File

LIPIcs.STACS.2008.1364.pdf
  • Filesize: 190 kB
  • 12 pages

Document Identifiers

Author Details

Felix Klaedtke

Cite AsGet BibTex

Felix Klaedtke. Ehrenfeucht-Fraissé Goes Automatic for Real Addition. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 445-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
https://doi.org/10.4230/LIPIcs.STACS.2008.1364

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.
Keywords
  • Automata theory
  • automata-based decision procedures for logical theories
  • upper bounds
  • minimal sizes of automata
  • linear arithmetic over the reals
  • f

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail