否定在高阶 Datalog 中的力量

我们考察了在 well-founded 语义和 stable model 语义下，Higher-Order Datalog$^\neg$ 的表达力，并建立了与复杂度类的紧密联系。我们证明，在 well-founded 语义下，对于所有 $k\geq 1$，$(k+1)$-Order Datalog$^\neg$ 捕获 k-EXP，该结果在输入数据库无显式排序情况下仍然成立。该事实的证明可通过使用该语言中强大的存在性谓词变量，或通过使用部分应用关系和关系枚举来实现。此外，我们展示了这种表达力在该语言的分层片段中得以保留。在 stable model 语义下，我们表明 $(k+1)$-Order Datalog$^\neg$ 通过谨慎推理捕获 co-(k-NEXP)，通过勇敢推理捕获 k-NEXP，分层片段增强了选择规则后亦得到类似结果。我们的结果建立了表达力的层次结构，突显了在高阶逻辑编程语境下，序数与非确定性之间有趣的权衡：在 well-founded 语义下，提高程序的序数可以超越 stable model 语义下较低序数程序的表达力。