Datalog 的单面统一是否足够？

问题描述

Datalog 很容易用 Prolog 的一个子集识别 不使用函数符号，而只使用常量和变量。 但是不使用否定的纯 Datalog 有一个进一步的约束（*）：

1. 每一个事实都是有根据的。
2. 规则头部中的每个变量也出现在规则主体中。

我们能否得出结论，单边统一就足以 回答分层 Datalog 查询？或者有没有例子，可以证明 SWI-Prolog 8.3.19 单面具有 (=>)/2

unfication，那是纯粹的 Datalog 但不以单面统一运行？

(*)
您一直想了解的有关 Datalog 的信息
塞里等阿尔。 - 1989
https://www.researchgate.net/publication/3296132

解决方法

答案是否定的。对于最简单的 Datalog 事实和查询，直接转换为单面 unfication 已经不起作用：

p(a).

?- p(X).
X = a

如果我们将 Prolog 事实 P 视为 P :- true，则通过 (=>)/2 将事实重写为 P => true。这东西不再工作了，用 SWI-Prolog 8.3.19 演示：

p(a) => true.

?- p(X).
ERROR: No rule matches p(_2556)

即使是 Picat 也被这个问题困扰，并且最初对事实进行了特殊处理。最近发布的 Picat v3 甚至重新引入了 Horn 子句。