How to express universal quantifier in the body of a datalog rule?

Question

I want to use universal quantifier in the body of a predicate rule, i.e., something like

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

It means that only if for each a from C(y, a), B(x,a) always has x to match (x,a), then A(x,y) is true.

Since in Datalog, every variable bounded in rule body is existential quantifier by default, the a would be an existential quantifier too. What should I do to express universal quantifier in the body of a predicate rule?

Thank you.

P.S. The Datalog engine I am using is logicblox.

Answer 1

The basic idea is to use the logical axiom

∀x φ(x) ⇔ ¬∃x ¬φ(x)

to put your rules in a form where only existential quantifiers are required (along with negation). Intuitively, this usually means computing the complement of your answer first, and then computing its complement to produce the final answer.

For example, suppose you are given a graph G(V,E) and you want to find the vertices which are adjacent to all others in the graph. If universal quantification were allowed in a Datalog rule body, you might write something like

Q(x) <- ∀y E(x,y).

To write this without the universal quantifier, you first compute the vertices which are not adjacent to all others

NQ(x) <- V(x), V(y), !E(x,y).

then return its complement as the answer

Q(x) <- V(x), !NQ(x).

The same kind of trick can be used in SQL, which also lacks universal quantifiers.