否定即失败

否定即失败（简称NAF）是逻辑编程中的一个非单调推理规则，用于推导出{displaystyle~p}，取决于推理算法的完整性，从而也取决于形式逻辑系统。取决于推理算法的完整性，因此也取决于形式逻辑系统。

从最早的Planner和Prolog开始，作为失败的否定就一直是逻辑编程的一个重要特征。在Prolog中，它通常使用Prolog的族外结构来实现。更广泛地说，这种否定被称为弱否定，与强否定（即明确的、可证明的）相反。

在Planner中，作为失败的否定可以按如下方式实现。如果（不是（目标p）），那么（断言¬p）。这就是说，如果证明p的穷举搜索失败，那么就断言¬p。这说明命题p在任何后续处理中都应被假定为不真实。然而，Planner不是基于一个逻辑模型，对前面的逻辑解释仍然是模糊的。

在纯Prolog中，NAF字元的形式为可以出现在子句的主体中，并且可以用来推导出其他NAF字词。例如，只给定四个子句

NAF的语义仍然是一个开放的问题，直到1978年，KeithClark表明它在逻辑程序的完成方面是正确的，其中，宽泛地讲，只有和NAF推理规则模拟了用完成度进行明确的推理，等价关系的两边都被否定了，右边的否定被分布到原子式上。例如，为了表明在非命题情况下，完成度需要用平等公理来增强，以正式确定具有不同名字的个体是不同的假设。NAF通过统一的失败来模拟这一点。例如，只给定两个子句用唯 一的名字公理和域封闭公理来增强。完成语义与包围法和封闭世界假设都密切相关。

完成语义证明了对结果的解释不被相信，就像在自体地方逻辑中一样。Gelfond和Lifschitz在1988年进一步发展了自体现象解释，它是答案集编程的基础。

带有NAF字元的纯Prolog程序P的自体语义是通过用一组地面（无变量）NAF字元Δ扩展P而得到的，在这个意义上是稳定的，即{displaystylep}的暗示。不是由P∪Δ所隐含的}。