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

Durand-Gasselin, Antoine ; Habermehl, Peter

Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree

pdf-format:
35.pdf (0.8 MB)

Abstract

Many relational structures are automatically presentable, i.e. elements of the domain can be seen as words over a finite alphabet and equality and other atomic relations are represented with finite automata. The first-order theories over such structures are known to be primitive recursive, which is shown by the inductive construction of an automaton representing any relation definable in the first-order logic. We propose a general method based on Ehrenfeucht-Fraïssé games to give upper bounds on the size of these automata and on the time required to build them. We apply this method for two different automatic structures which have elementary decision procedures, Presburger Arithmetic and automatic structures of bounded
degree. For the latter no upper bound on the size of the automata was known. We conclude that the very general and simple automata-based algorithm works well to decide the first-order theories over these structures.

BibTeX - Entry

@InProceedings{durandgasselin_et_al:LIPIcs:2012:3419,
  author =	{Antoine Durand-Gasselin and Peter Habermehl},
  title =	{{Ehrenfeucht-Fraiss{\'e} goes elementarily automatic for structures of bounded degree}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{242--253},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{Christoph D{\"u}rr and Thomas Wilke},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3419},
  URN =		{urn:nbn:de:0030-drops-34198},
  doi =		{10.4230/LIPIcs.STACS.2012.242},
  annote =	{Keywords: Automata-based decision procedures for logical theories, Automatic Structures, Ehrenfeucht-Fraiss{\'e} Games, Logics, Complexity}
}

Keywords: Automata-based decision procedures for logical theories, Automatic Structures, Ehrenfeucht-Fraïssé Games, Logics, Complexity
Collection: 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)
Issue Date: 2012
Date of publication: 24.02.2012

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