datalog - 如何在数据记录规则的主体中表达全称量词？

Question

我想在谓词规则的主体中使用通用量词，即类似

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。

Answer 1

基本思想是使用逻辑公理

∀ x φ( x ) ⇔ ¬∃<em>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 中。