Ehrenfeucht-Fra¨ıss´e goes elementarily automatic for structures of bounded degree
Ehrenfeucht-Fra¨ıss´e goes elementarily automatic for structures of bounded degree
复制标题
Ehrenfeucht-Fra´ıss´e 对于有界度结构来说基本上是自动的
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
P. Habermehl
中科院分区：
文献类型：
--
作者：
Antoine Durand;P. Habermehl
许多关系结构是自动可表示的，即域的元素可以被看作是有限字母表上的单词，等式和其他原子关系可以用有限自动机表示。在这样的结构上的一阶理论被认为是原始递归的，这可以通过表示一阶逻辑中可定义的任何关系的自动机的归纳构造来证明。我们提出了一个通用的方法，基于Escherifeucht-Fraïssé游戏，这些自动机的大小和所需的时间来建立它们的上限。我们将这种方法应用于两种不同的自动结构，这两种自动结构具有基本的决策过程，Presburger算法和有界度的自动结构。对于后者没有上限的大小的自动机是已知的。我们的结论是，非常一般和简单的基于自动机的算法可以很好地确定这些结构的一阶理论。1998
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. 1998