公理决议

Question

我试着理解公理解析如何在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是相同的操作(即相同的签名但不是相同的操作数),则对每个操作数应用算法,如果找到每个操作数的解,则找到解.

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

提前致谢

Answer 1

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中有一些关于评估顺序(从左到右)和"剪切"(修剪搜索树)的特殊规则,但这个细节超出了本简要教程的范围.

现在,要确定a是否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教科书!

希望这可以帮助.