我熟悉Prolog将否定实现为NaF，甚至它对NaF的实现也是不完整的，尤其是与非地面否定文字的挣扎。我这里的问题是关于特定的语义。假设您有一个子句p(X) :- q(Y).这是 \A x，y(q(y( -> p(x(( 的幽闭形式，即 \E y q(y( -> \A x p(x(，这确实是 prolog 实现的语义。但是现在考虑我是否有p(X) :- + q(Y).在 FOL 中，这将表示为 \E y ~q(y( -> \Ax p(x( 即"如果 q 对某个 y 失败，则 p 对每个 x 都成立"，但这似乎不是 Prolog 实现的语义。相反，Prolog 将要求 q 在成功之前对每个 y 进行有限失败+ q(y)并且 p 对于任何 x 都是真的。因此，它的语义似乎非常不同，而不仅仅是不完整。我错过了什么吗？
谢谢
在Prolog中，p(X) :- + q(Y).本身并不能充分表达这样一个概念，即如果q在某些Y失败，p对每个X都成立，因为Prolog不知道有资格测试q的Y值的可能范围。因此，它不知道任何q(Y)无法证明的Y值。
但是，假设您有以下内容：
q(a).
q(b).
q(c).
valid_y(Y) :- member(Y, [a,b,c,d,e]).
然后你可以写：
p(_) :- valid_y(Y), + q(Y).
然后p(_)成功了两次，因为Prolog寻求所有解决方案。您可以使用剪切或once/1来避免这种情况。