发生检查

在计算机科学中，发生检查是句法统一算法的一部分。如果S包含V，它将导致一个变量V和一个结构S的统一失败。

在定理证明中，没有发生检查的统一会导致不健全的推理。例如，Prolog的目标X=f(X){displaystyleX=f(X)}就会成功，将X绑定到一个循环上。作为另一个例子，在没有发生检查的情况下，一个解析证明会将X绑定到Herbrand宇宙中没有对应的循环结构上。

没有发生检查，就可以为非定理找到一个解析证明有理树统一Prolog的实现通常出于效率的考虑而省略了发生检查，这可能会导致循环数据结构和循环。由于不执行发生检查，统一一个术语的最坏情况下的复杂度为现代的实现，基于Colmerauer的PrologII。

使用有理树统一来避免循环。然而，在存在循环项的情况下，很难保持复杂性时间的线性。可以很容易地构建Colmerauer算法变得二次的例子，但也存在完善的建议。

统一（计算机科学）#中给出的统一算法的运行实例见图片，试图解决目标的统一算法然而，没有发生检查规则（在那里被命名为检查）；应用消除规则反而导致最后一步的循环图（即一个无限的项）。

ISOProlog实现有内置的谓词unify_with_occurs_check/2用于健全的统一，但是当统一被调用时，可以自由地使用不健全的甚至是循环的算法，只要该算法对所有不受发生检查(NSTO)的情况正确工作。

内置的acyclic_term/1用于检查术语的有限性。为所有统一提供健全统一的实现是Qu-Prolog和StrawberryProlog以及（可选择通过运行时标志）。XSB、SWI-Prolog、TauProlog和ScryerProlog。各种各样的优化可以使声音统一在普通情况下变得可行。