如何在数据模拟规则的正文中表示通用量词？

Question

我想在谓词规则的正文中使用通用量词，例如

A(x，y) <-∀B(x，a)，C(y，a)

这意味着，只有对于来自C(y，a)，B(x，a)的每个都有x匹配(x，a)，那么A(x，y)才是真。

由于在Datalog中，规则主体中的每个有界变量默认都是存在量词，因此a也将是存在量词。我应该做什么来表达谓词规则正文中的通用量词？

谢谢。

我正在使用的Datalog引擎是logicblox。

Answer 1

其基本思想是使用逻辑公理。

∀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中也可以使用同样的技巧，因为SQL也缺乏通用的量词。