我想在谓词规则的主体中使用全称量词，例如
A(x,y) <- ?B(x,a), C(y,a)。
这意味着只有对于来自 C(y, a ) 的每个a，B(x, a ) 总是有 x 匹配 (x, a )，那么 A(x,y) 为真。
由于在 Datalog 中，规则体中的每个变量默认都是存在量词，因此a也将是存在量词。我应该怎么做才能在谓词规则的主体中表达全称量词？
谢谢你。
PS 我使用的 Datalog 引擎是 logicblox。
基本思想是使用逻辑公理
? x ?( x ) ? ～？x ¬?( x )
将您的规则置于只需要存在量词（连同否定）的形式中。直观地说，这通常意味着首先计算答案的补码，然后计算其补码以生成最终答案。
例如，假设您有一个图G ( V , E )，并且您想找到与图中所有其他顶点相邻的顶点。如果 Datalog 规则体中允许通用量化，您可能会编写类似
Q(x) <- ?y E(x,y).
要在没有全称量词的情况下编写此代码，您首先要计算与所有其他顶点不相邻的顶点
NQ(x) <- V(x), V(y), !E(x,y).
然后返回它的补码作为答案
Q(x) <- V(x), !NQ(x).
同样的技巧也可以用在 SQL 中，它也缺少全称量词。