YAP Prolog 中的正向链接?

Ser*_*gio 5 prolog

我需要在某些 Prolog 问题中使用前向链接器。我想避免使用原版元解释器从头开始实现它(但如果没有其他选项可用,我将不得不这样做),因为使用元解释器执行此操作会很慢,而且我我确信应该有一些好的实现。有人知道 YAP 或 SWI Prolog 是否包含本机且高效的前向链接器吗?如果是这种情况,将不胜感激如何安装/使用它的指针。

如果这两个 Prolog 引擎上没有可用的本地前向链接器,有人可以向我推荐一个基于 vanilla 元解释器的好的开源实现,我可以将其用作外部 Prolog 库吗?

提前致谢。

Tra*_*ers 5

让我们根据最小逻辑而不是解析定理证明来解释反向链接和正向链接。正常的反向链接 Prolog 规则可以看作是最小逻辑的左蕴涵引入规则的应用。所以基本上当我们有一个目标 P 和一个规则 A->P 时,组合推理规则说我们可以用目标 A 替换目标 P:

-------- (Id)
P |- P            G, A -> P |- A
--------------------------------- (Left ->)
        G, A -> P |- P
Run Code Online (Sandbox Code Playgroud)

现在可以使用相同的规则来为正向链接应用程序建模。这次我们没有目标 P,而是在前提中实现了条件 A。当存在规则 A -> P 时,该规则也允许我们实现头部 P。组合推理规则如下:

------- (Id)
A |- A            G, A, A -> P, P |- B
--------------------------------------- (Left ->)
         G, A, A -> P |- B
Run Code Online (Sandbox Code Playgroud)

我们的小程序的想法是完全计算前向链接过程的固定点 F(M) = M。我们所做的是计算迭代 M0、M1、M2 等。这仅在过程以有限结果终止时才有效。从演绎数据库中,我们采用了仅计算 Mn+1 和 Mn 之间的增量的想法。有可能找到一个 G,因此 F(Mn)\Mn = G(Mn\Mn-1,Mn-1) 相对较少的努力。

G 的当前实现可能会遇到循环数据,因为当前没有消除重复项。在还允许删除事实的前向链接器中,可以使用特殊的前向规则来消除重复项。成熟的前向链系统无论如何都应该允许删除事实,然后它们甚至可以用于实现约束求解系统。

但是,让我们暂时保留简单的想法和相应的简单代码。

来自 F 函数的 G 函数(delta/2)(原始规则)
http://www.xlog.ch/jekejeke/forward/delta.p

具有前向链的玩具专家系统
http://www.xlog.ch/jekejeke/forward/expert.p


Nic*_*ain 5

YAP 和 SWI 都包含约束处理规则的实现 - http://dtai.cs.kuleuven.be/projects/CHR/ - 这是一个前向链规则系统。

我不能谈论它在您的特定问题上的表现,但众所周知 CHR 是有效的(请参阅 CHR 网站上链接的论文)。

CHR 还具有 Java、Haskell 和 C 实现,因此如果您以后需要更好的性能,您可以轻松地将规则移植到其中一种语言。

  • 其中一篇关于 CHR 的 C 实现的论文包括一些比较 SWI、Java 和 C 版本的基准 - http://people.cs.kuleuven.be/~pieter.wuille/static/chr07.pdf。看起来 SWI 和 Java 具有可比性,而 C 则要快得多。 (2认同)