论文标题
关于检查检查的注释（扩展报告）
A note on occur-check (extended report)
论文作者
论文摘要
我们削弱了“不接受检查”（NSTO）的概念，该概念避免了逻辑编程中发生检查的大多数已知结果。 NSTO意味着仅在此类原子上执行统一，而在非确定统一算法的任何运行中，发生的检查都永远不会成功。在这里，我们证明“任何运行”可以削弱“某些运行”。我们提出了一些相关的足够条件，可以安全地省略该检查。我们展示了所提出的方法提供的示例比基于良好的方法且适应良好的程序提供了更多的一般结果（这包括后一种方法不适用的情况）。我们还基于NSTO提出了足够的条件，为任意选择规则工作。
We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that "any run" can be weakened to "some run". We present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable). We additionally present a sufficient condition based on NSTO, working for arbitrary selection rules.
