如何在不证明某些东西是错误的的情况下使规则失败

Question

我正在尝试制作一个invert/2。我希望它忽略其论证的顺序，这样你就不必担心反转的哪一半是你知道的，这样你就不必在将反转陈述为事实时重复自己。我目前有

invert(Left, Right) :-
    call_with_depth_limit(invert(Right, Left), 1, Result),
    Result = depth_limit_exceeded.

作为第一invert规则。这大多有效，但如果invert(a, b).，那么?- invert(b, X).既能提供X = a，又能false，这根本不是我想要的。

Answer 1

我会考虑两件事。首先，确保您为在事实中建立关系的对称性而创建的谓词的名称与事实的名称不同。名称相同通常会导致无限递归等问题。其次，如果事实在你控制范围内申报，对事实是否明确申报对称案件要保持一致。如果他们这样做，那么你不需要额外的谓词。如果没有，那么您需要一个额外的谓词。

例如，显式声明对称性：

opposite(a, b).
opposite(b, a).
opposite(c, d).
opposite(d, c).

您不需要额外的谓词即可获得opposite的对称解。

未显式声明对称性的示例：

opposite(a, b).
opposite(c, d).
inverted(X, Y) :- opposite(X, Y).
inverted(X, Y) :- opposite(Y, X).

在这种情况下，查询inverted/2而不是opposite/2将处理关系中的对称性。