14

我已经阅读了很多关于 Prolog 的Negation by Failure的文章，其中 Prolog 为了证明\+Goal持有试图证明Goal失败。

这与CWA（近距离世界假设）高度相关，例如，如果我们查询\+P(a)（哪里P是 arity 1 的谓词）并且我们没有线索可以证明P(a)Prolog 假设（由于 CWA）是not P(a)成功\+P(a)的。

根据我的搜索，这是一种解决经典逻辑弱点的方法，如果我们不知道P(a)那么我们就无法回答是否\+P(a)成立。

上面描述的是在 Prolog 中引入非单调推理的方式。此外，有趣的部分是克拉克证明了失败的否定与经典否定仅适用于基础条款兼容/相似。我理解，例如：

X=1, \+X==1.: 应该在 Prolog（和经典逻辑）中返回 false。

\+X==1, X=1.: 在经典逻辑中应该返回 false 但在 Prolog 中成功，因为检查 NF 的时间不受限制X，这与经典纯逻辑不同。

\+X==1.：不应该在经典逻辑中给出任何答案，直到X被绑定，但在 Prolog 中它返回 false（可能是为了打破经典逻辑的弱点），这与纯逻辑不同/不兼容。

我的尝试是模拟经典的否定，感谢@false 在评论中的建议，当前的实现是：

\\+(Goal) :- when(ground(Goal), \+Goal).

一些测试：

?- \\+(X==1).
when(ground(X), \+X==1).

?- X=1, \\+(X==1).
false.

?- \\+(X==1), X=1.
false.

我的问题：

以上是对经典否定的正确解释吗？（它是否遗漏了任何明显的极端情况？？我也担心使用时when/2的逻辑纯度，可以安全地假设上述内容是纯粹的吗？？）。

4

2 回答 2

3

Prolog 不能做经典的否定。因为它不使用经典推理。即使存在克拉克完成，它也无法检测到以下两个经典定律：

不矛盾定律：~(p /\ ~p)

排中律：p \/ ~p

这是一个示例，以这个逻辑程序和这些查询为例：

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

逻辑程序的 Clark 补全如下，作为失败查询执行的否定产生以下结果：

   p <-> p

   loops

   loops

克拉克补全解决了谓词定义和负面信息的问题。另请参阅第5.2 节规则及其完成。另一方面，当周围没有谓词定义时，当否定运算符定义为 deMorgan 样式时，CLP(X) 有时可以同时执行这两个定律。这是 CLP(B) 的否定运算符：

?- listing(neg/1).
neg((A;B)) :-
    neg(A),
    neg(B).
neg((A, _)) :-
    neg(A).
neg((_, A)) :-
    neg(A).
neg(neg(A)) :-
    call(A).
neg(sat(A)) :-
    sat(~A).

这是一些执行：

?- sat(P); neg(sat(P)).
P = 0 
P = 1.
?- neg((sat(P), neg(sat(P)))).
P = 0 
P = 1.

当否定影响域时，CLP(X) 也会出现问题，这些域通常是有限的，然后会变得无限。因此，例如 (#=)/2, ... 之类的约束不应该成为问题，因为它可以被约束 (#\=)/2, ... 替换。

但是当应用于约束 (in)/2 时，对 CLP(FD) 的否定通常不起作用。如果 CLP(X) 系统提供具体化，这种情况可以稍微缓解。在这种情况下，析取可以比仅使用 Prolog 回溯析取更智能一点。

于 2018-01-18T02:18:26.413 回答
1

在 SWI-Prolog 中，可以实现约束处理规则中经典逻辑的推理规则，包括德摩根定律和不矛盾定律：

:- use_module(library(chr)).
:- chr_constraint is_true/1.
:- chr_constraint animal/2.
:- initialization(main).
:- set_prolog_flag('double_quotes','chars').

is_true(A),is_true(A) <=> is_true(A).
is_true(A=B) ==> A=B.
is_true(A\=B) ==> not(A=B).
is_true(not(A)),is_true(A) ==> false.
is_true(not((A;B))) ==> is_true((not(A),not(B))).
is_true(not((A,B))) ==> is_true((not(A);not(B))).
is_true((A,B)) ==> is_true(A),is_true(B).
is_true((A;B)) ==> is_true(A),(is_true(B);is_true(not(B)));is_true(B),(is_true(A);is_true(not(A))).
is_true(not(not(A))) ==> is_true(A).

然后，您可以像这样使用求解器：

is_true(animal(X,A)),is_true(animal((Y,A))) ==> X \= Y,false;X==Y.
is_true((A->B)) ==> is_true(((A;not(A)),B));is_true(((not(A);A),not(B))).

main :- is_true(((X=cat;X=dog;X=moose),(not((animal(dog,tom);animal(moose,tom))),animal(X,tom)))),writeln(animal(X,tom)).

该程序打印animal(cat,tom).

但这个公式可以使用不同的算法更有效地求解，例如DPLL。

于 2021-04-21T17:59:31.053 回答