关于单调谓词的推理

**** 可以通过应用声明性推理来调试单调谓词。

在纯 Prolog 中，编程错误可能导致以下一种或所有现象：

1. 谓语不正确成功的情况下，它应该会失败
2. 谓语错误失败的情况下，它应该获得成功
3. 谓词意外地循环，它应该只产生一组有限的答案。

作为一个例子，考虑如何通过声明性推理调试 case(2)：我们可以系统地删除谓词的子句的目标，并查看查询是否仍然失败。在单调代码中，删除目标最多可以使得结果程序更加通用。因此，我们可以通过查看哪些目标导致意外故障来查明错误。