Datalog-Expressibility for Monadic and Guarded Second-Order Logic
Manuel Bodirsky, Simon Knäuer and Sebastian Rudolph
我们描述了Monadic二阶逻辑(MSO)中的句子,这些句子在存在鹅卵石游戏中等同于Datalog程序的有限结构。 我们还表明,对于可以在MSO中表达并在同态下关闭的每个类有限结构的C类,对于所有整数l,k,在Feder和Verdi的意义上存在一个规范的宽度(l,k)数据程序Pi。 相同的特征也适用于受保护的二阶逻辑(GSO),它正确地扩展了MSO。 为了证明我们的结果,我们表明GSO中的每一个C类,其补充在同态下是约束满意度问题(CSP)的有限结合,可数分类结构。 众所周知,MSO和Datalog的交集包含嵌套monadically定义查询(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 ...