NU-Prolog 和哥德尔逻辑合理的“if-then-else”扩展

Question

A paper about mercury 表示如下：

The if-then-else and negation constructs in most variants of Prolog are non-logical and unsound: they can cause the system to compute answers which are inconsistent with the program viewed as a logical theory. Some existing logic programming systems such as NU-Prolog and Gödel provide logical and sound replacements for these Prolog constructs. Unfortunately, these systems enforce safety via runtime groundness checks. This effect can increase the runtime of a program by an arbitrarily large factor; if the goals checked for groundness include large terms, the checks can be prohibitively expensive.

NU-Prolog 和 Gödel 看起来相当死气沉沉而且不自由，但我仍然想知道：

这些合乎逻辑且合理的 if-then-else 替换是什么？
他们在 SWI 或 GNU Prologs 中有类似物吗？
它们是如何工作的？它们如何工作？向 Prolog 添加逻辑否定会将其变成一般 FOL，对吗？您基本上需要一个通用的 FOL 定理证明器才能使用它？
它们与 if_/3? if_/3 不同吗？必须扩展才能在新条件下使用。在 NU-Prolog 和 Gödel 中是否也必须这样做？

Answer 1

if-then-else 的突破可能是一个新的注解。通过注释我理解了模式声明之类的东西，确定性声明等。对于 if then else，a 完整的声明会很好。让我们假设我们可以声明谓词或内置 p/n 完成。这个会意味着它有属性用于基础参数 t1,..,tn:

   T |- p(t1,..,tn)

- or -

   T |- ~p(t1,..,tn)

或者简而言之，如果理论 T 是递归可枚举的，那么它将是一个可判定的谓词。如果我们再回想一下 if-then-else 在逻辑上是：

    ITE(A,B,C) == (A => B) & (~A => C)

然后我们可以使用完整的注释如下。让我们假设 A = p(t1,..,tn)。由于注释 Prolog 系统会尝试证明 A。如果它没有成功，因为的完整注释，Prolog 系统可以推断出 ~A 会成功。因此它可以使用 else 分支没有 ~A.

的证明尝试

但有趣的是，这已经是 ISO 核心标准的 if-then-else 做，(A->B;C) 也只证明一次。所以有什么问题？我想问题是 A 可能更复杂，不一定是地面。或者甚至谓词 p/n 可能不完整，或者我们甚至不知道它是否完整。总之 ISO 核心标准仍然允许这些情况我们使用 (A->B;C).

接地问题有时可以通过使用运行时来解决接地检查。这大概就是Mercury所指的：

    when(ground(A), (A->B;C))

SWI-Prolog 甚至使用了一个技巧来制作接地检查更便宜，另请参阅 Discourse 上的进一步 discussion：

%!  trigger_ground(@Term, :Goal)
%
%   Trigger Goal when Term becomes   ground.  The current implementation
%   uses nonground/2, waiting for an   atribtrary  variable and re-check
%   Term  when  this  variable   is    bound.   Previous   version  used
%   term_variables and suspended  on  a   term  constructed  from  these
%   variables. It is clear  that  either   approach  performs  better on
%   certain types of terms. The term_variables/2  based approach wins on
%   large terms that are almost  ground.   Possibly  we need a nonground
%   that also returns the number of tests   performed  and switch to the
%   term_variables/2 based approach if this becomes large.

trigger_ground(X, Goal) :-
    (   nonground(X, V)
    ->  '$suspend'(V, when, trigger_ground(X, Goal))
    ;   call(Goal)
).

Answer 2

我找到了这篇关于 MU- 和 NU-Prologs 的评论 here，如果有人感兴趣：

NU-Prolog 和哥德尔逻辑合理的“if-then-else”扩展

NU-Prolog's and Gödel's logical and sound `if-then-else` extension

prolog

logic-programming

logical-purity