×

Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. (English) Zbl 1245.03061

Dürr, Christoph (ed.) et al., STACS 2012. 29th international symposium on theoretical aspects of computer science, Paris, France, February 29th – March 3rd, 2012. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-35-4). LIPIcs – Leibniz International Proceedings in Informatics 14, 242-253, electronic only (2012).
Summary: 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.
For the entire collection see [Zbl 1237.68016].

MSC:

03D05 Automata and formal grammars in connection with logical questions
03B25 Decidability of theories and sets of sentences
03C13 Model theory of finite structures
03C57 Computable structure theory, computable model theory
PDFBibTeX XMLCite
Full Text: DOI