题

我试图了解公理分辨率如何在prolog中起作用。

假设我定义了自然数的两个基本操作：

  • s（术语）（代表继任者）和

  • 添加（术语，另一个术语）。

添加的语义由

  • 添加（0，x1） - > x1

  • 添加（x1，0） - > x1

  • 添加（s（x1），y1） - > s（add（x1，y1））

然后，我想解决方程式

添加（x，add（y，z））= s（0）

我想一个策略可能是

  • 测试方程的右侧（RHS）是否等于其左侧（LHS）

  • 如果看不出是否可以通过寻找最通用的统一器来找到解决方案

  • 如果没有，请尝试找到可以在此方程式中使用的公理。做这项工作的策略可能是（对于每个公理）：尝试求解等式的RHS等于公理的RHS。如果有解决方案，则尝试求解方程的LHS等于公理的LHS。如果成功，我们找到了正确的公理。

  • 最终，如果没有解决方案，并且方程的LHS和RHS是相同的操作（即相同的签名，而不是相同的操作数），则在每个操作数上应用算法，并且如果找到每个操作数的解决方案，则发现解决方案。

我认为（简单）算法可能会起作用。但是，我想知道是否有人有解决此类问题的经验？有人知道我可以在哪里找到有关更好算法的文档吗？

提前致谢

有帮助吗？

解决方案

您要寻找的是 变窄. 。它以某些功能性语言实现 咖喱, ，但不在序言本身中。

其他提示

Prolog程序是谓词的集合。

谓词是一系列条款。

条款具有表格

Head :- Body.

意义 ”Head 如果是真的 Body 是真的”。

有一个速记条款形式

Head.

这意味着与

Head :- true.

在哪里 true 是一个始终是真实的内置。

回到 Body 条款的一部分， Body 是一个可以采用以下表格之一的目标（A, B, ， 和 C 表示任意目标）：

Atom            % This is true if Atom is true (see below).
A, B            % This is true if A is true and B is true.
(A ; B)         % This is true if A is true or B is true.
\+ A            % This is true if A is not true.
(A -> B ; C)    % If A is true then B must be true, else C must be true.

序言中有一些有关评估顺序（从左到右）和“剪切”（修剪搜索树）的特殊规则，但这是本简短教程的范围之外的细节。

现在，决定是否 Atom 是真的， Atom 可以是以下表格之一（X 和 Y 表示任意条款）：

true                % or some other builtin with given truth rules.
X = Y               % True if X and Y are successfully unified.
p(X, Y, ...)        % True if p(X, Y, ...) matches the head of some clause
                    % and the Body is true.

本质上，一个术语是任何语法。

在这里要发现的关键是，Prolog没有功能！您可以使用功能性语言定义功能 add(X, Y) 评估的总和 X 和 Y, ，在Prolog中，您定义了一个头部的谓词 add(X, Y, Z) 如果成功，那就统一了 Z 带有表示总和的一词 X 和 Y.

鉴于所有这些，我们可以在Prolog中定义您的规则如下：

add(0, Y, Y).                        % 0 + Y = Y.
add(Y, 0, Y).                        % Y + 0 = Y.
add(s(X), Y, s(Z)) :- add(X, Y, Z).  % s(X) + Y = s(X + Y).

我在哪里使用 0 表示零（！）和 s(X) 表示 X.

考虑评估 add(s(s(0)), s(0), Z):

add(s(s(0)), s(0), Z)                 % Only the third head for add matches, so...
---> Z = s(Z0), add(s(0), s(0), Z0).

add(s(0), s(0), Z0)                   % Only the third head for add matches, so...
---> Z0 = s(Z1), add(0, s(0), Z1).

add(0, s(0), Z1)                      % Only the first head for add matches, so...
---> Z1 = s(0).

将所有这些统一 Z 在一起，我们有 Z = s(s(s(0))).

现在，您可能会问“如果子句中有多个头部匹配的情况会发生什么”或“如果评估路径失败，会发生什么？ Prolog教科书！

希望这可以帮助。

Brachmann和Levesque的“知识代表和推理”给出了相当不错的介绍。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top