公理消解

Question

公理消解

algorithmprologaxiomsuccessor-arithmetics

3

我试图理解Prolog中公理解析的工作原理。

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

- 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是相同的操作（即具有相同的签名但不是相同的操作数），则对每个操作数应用算法，如果每个操作数都有解决方案，则找到解决方案。

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

提前感谢您的帮助。

- bob bajram

看起来又像是 Erlang，现在的 Prolog 老师怎么了？ - user502187

3个回答

2

你正在寻找的是narrowing。它在一些函数逻辑语言（如Curry）中实现，但在Prolog本身中并没有实现。

- starblue

0

"知识表示与推理" 一书由布拉赫曼和勒韦斯克编写，对这些内容的工作原理进行了相当好的介绍。

- cadolphs

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Rafe · Accepted Answer

Prolog程序是谓词的集合。

谓词是子句的集合。

子句的形式为

Head :- Body.

今日免费次数已满, 请开通会员/明日再来

Head.

这意味着与...相同

Head :- true.

where 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教材！

希望这能帮到你。