非单调谓词

以下是不是单调的谓词示例 ：

• 像 var/1，integer/1 等的元逻辑谓词
• 术语比较谓词如 (@<)/2 和 (@>=)/2
• 谓词使用 !/0，(\+)/1 和其他打破单调性的结构
• 所有解决方案的谓词如 findall/3 和 setof/3。

如果使用这些谓词，那么添加目标可能会导致更多的解决方案，这与逻辑中已知的重要声明性属性相反，即添加约束最多可以减少，从不扩展解决方案集。

因此，我们依赖于声明性调试和其他推理的其他属性也会被破坏。例如，非单调谓词打破了从一阶逻辑中已知的连词交换的基本概念。以下示例说明了这一点：

?- var(X), X = a.
X = a.

?- X = a, var(X).
false.

像 findall/3 这样的全解决方案谓词也打破了单调性： 添加条款可能会导致之前持有的目标失败。这也与从一阶逻辑中已知的单调性背道而驰，其中添加事实最多可以增加，而不会减少后果集。 ** ** ** **