论文标题
单核和守卫二阶逻辑的数据表可表达性
Datalog-Expressibility for Monadic and Guarded Second-Order Logic
论文作者
论文摘要
我们在Monadic二阶逻辑（MSO）中表征了句子，这些句子与存在的卵石游戏有关，这些句子与数据编写程序相等的有限结构。我们还表明，对于每个可以用MSO表示的有限结构的C级C，在同构中封闭，对于所有整数l，K，都存在一个规范的数据元素pi PI宽度（L，K），从Feder和Verdi的意义上讲。适当扩展MSO的卫星二阶逻辑（GSO）也具有相同的特征。为了证明我们的结果，我们表明，GSO中的每个C级C级的补体在同态下封闭是有限的，这些结构是有限的约束满意度问题（CSP）的有限结合。已知MSO和Datalog的相交包含嵌套的单声界定义查询（Nemodeq）的类别；同样，我们表明GSO和Datalog的交集包含所有可以通过嵌套保护的查询语言表达的所有问题。然而，通过利用我们的结果，我们可以证明两种查询语言都无法用作表征，因为我们在MSO和Datalog的交叉点上展示了在嵌套的保护查询中无法表达的查询。
We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all integers l,k, there exists a canonical Datalog program Pi of width (l,k) in the sense of Feder and Verdi. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of countably categorical structures. The intersection of MSO and Datalog is known to contain the class of nested monadically defined queries (Nemodeq); likewise, we show that the intersection of GSO and Datalog contains all problems that can be expressed by the more expressive language of nested guarded queries. Yet, by exploiting our results, we can show that neither of the two query languages can serve as a characterization, as we exhibit a query in the intersection of MSO and Datalog that is not expressible in nested guarded queries.
