一元逻辑与带保护条件的二阶逻辑的数据表表达能力

《ACM Transactions on Computational Logic》：Datalog-Expressibility for Monadic and Guarded Second-Order Logic

本文通过存在性石子游戏刻画了有限结构上等价于Datalog程序的MSO句子，并将结果扩展到GSO。证明其补集封闭类可表示为有限CSP的并，且Nemodeq和GQ+无法完全characterize所有相关问题。

　　

摘要

我们利用存在性鹅卵石博弈（existential pebble game）来描述在单子二阶逻辑（Monadic Second-order Logic, MSO）中那些对应于Datalog程序的有限结构上的句子。我们还证明了：对于每一个可以用MSO表达的有限结构类，并且该类在同态下是封闭的，存在一个“规范的”（canonical）Datalog程序，其宽度满足特定条件。此外，对于所有的自然数$m, k \in \mathbb{N}$，也存在这样的Datalog程序。同样的特征也适用于Guarded Second-order Logic（GSO），它是MSO的扩展形式。为了证明我们的结果，我们展示了在GSO中，每一个其补集在同态下封闭的类都可以表示为一系列约束满足问题（Constraint Satisfaction Problems, CSPs），这些约束满足问题对应于某些特定的结构类型。已知MSO与Datalog的交集包含了“嵌套单子定义的查询”（Nested Monadically Defined Queries, Nemodeq）类；同样，我们也证明了GSO与Datalog的交集包含了所有可以用更强大的语言“嵌套保护查询”（Nested Guarded Queries, GQ）表达的问题。然而，通过利用我们的结果，我们可以证明这两种查询语言都无法作为这类问题的完整表征工具，因为我们构造了一个CSP，其补集对应于一个在MSO与Datalog的交集中存在的查询，而这个查询无法用GQ语言表达。