3

我试图了解公理解析在 prolog 中是如何工作的。

假设我定义了自然数的两个基本运算：

  • s(term)（代表继任者）和

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

add 的语义由下式给出

  • 添加 (0, x1) -> x1

  • 添加 (x1, 0) -> x1

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

然后，我想解方程

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

我想一种策略可能是

  • 测试等式的右手边 (RHS) 是否等于其左手边 (LHS)

  • if not 看看是否可以通过寻找最通用的统一器找到解决方案

  • 如果不是，那么尝试找到一个可以在这个方程中使用的公理。完成这项工作的策略可能是（对于每个公理）：尝试求解方程的 RHS 等于公理的 RHS。如果有解，则尝试求解方程的 LHS 等于公理的 LHS。如果它成功了，那么我们就找到了正确的公理。

  • 最终，如果没有解，并且方程的 LHS 和 RHS 是相同的操作（即相同的签名但不同的操作数），则将算法应用于每个操作数，如果为每个操作数找到解，则找到解。

我认为这个（简单的）算法可能有效。但是，我想知道是否有人有解决此类问题的经验？有谁知道我在哪里可以找到一些关于更好算法的文档？

提前致谢

4

3 回答 3

4

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.

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

现在，要确定 an 是否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的总和的术语统一。XY

鉴于这一切，我们可以在 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))).

现在，您可能会问“如果一个子句中有多个头部匹配会发生什么”或“如果评估路径失败会发生什么？”，答案是“不确定性”、“回溯”，一般来说，阅读一个序言教科书！

希望这可以帮助。

于 2010-11-30T23:20:48.963 回答
2

您正在寻找的是所谓的缩小。它是在一些功能逻辑语言中实现的，例如Curry，但不是在 Prolog 本身中实现的。

于 2010-12-01T07:30:09.557 回答
0

Brachmann 和 Levesque 的“知识表示和推理”很好地介绍了这些东西的工作原理。

于 2010-11-30T22:01:21.427 回答