公理分辨率

Question

我尝试了解公理解析在序言中的工作原理。

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

• s(term)（代表后继）和

• add(term, anotherTerm) .

add 的语义由

• add(0, x1) ->; 给出。 x1

• add (x1, 0) ->; x1

• add(s(x1), y1) -> s(add(x1, y1))

然后，我想求解方程

add (x, add(y, z)) = s(0)

我想一种策略可能是

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

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

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

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

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

提前致谢

Answer 1

Prolog 程序是谓词的集合。

谓词是子句的集合。

子句的形式

Head :- Body.

表示“如果 Body 为 true，则 Head 为 true”。

有一个简写子句形式

Head.

相同

Head :- true.

，其含义与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 中有一些关于求值顺序（从左到右）和“剪切”（修剪搜索树）的特殊规则，但这只是细节这超出了本简短教程的范围。

现在，要确定 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教科书！

希望这有帮助。

Answer 2

您正在寻找的内容称为缩小< /a>.它在一些功能逻辑语言中实现，例如 Curry，但在Prolog 本身。

Answer 3

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