在計算機科學中，發生檢查是句法統一算法的一部分。如果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。各種各樣的優化可以使聲音統一在普通情況下變得可行。