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

Question

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

A(x,y) <- ∀B(x,a), C(y,a).

这意味着只有当每个 从 C(y, a ), B(x, a ) 总是有 x 匹配 (x, a , ), 然后是 A(x, a )是真的。

因为在 Datalog 中，规则体中的每个变量默认都是存在量词， 也将是一个存在量词。我应该怎么做才能在谓词规则的主体中表达全称量词？

谢谢你。

附言我使用的 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 中，它也缺少全称量词。