Application in theorem proving
In theorem proving, unification without the occurs check can lead to unsound inference. For example, the Prolog goal will succeed, binding X to a cyclic structure which has no counterpart in the Herbrand universe. As another example,  without occurs-check, a resolution proof can be found for the non-theorem  : the negation of that formula has the conjunctive normal form , with and denoting the Skolem function for the first and second existential quantifier, respectively; the literals and are unifiable without occurs check, producing the refuting empty clause.
By default, Prolog implementations usually omit the occurs check for reasons of efficiency, which can lead to circular data structures and looping. By not performing the occurs check, the worst case complexity of unifying a term with term is reduced from to ; in particular, the frequent case of variable-term unifications, runtime shrinks to . 
A naive omission of the occurs check leads to the creation of cyclic structures and may cause unification to loop forever. Modern implementations, based on Colmerauer's Prolog II,     use rational tree unification to avoid looping. See image for an example run of the unification algorithm given in Unification (computer science)#A unification algorithm, trying to solve the goal , however without the occurs check rule (named "check" there); applying rule "eliminate" instead leads to a cyclic graph (i.e. an infinite term) in the last step.
ISO Prolog implementations have the built-in predicate unify_with_occurs_check/2 for sound unification but are free to use unsound or even looping algorithms when unification is invoked otherwise. Implementations offering sound unification for all unifications (optionally, via a runtime flag) are ECLiPSe, XSB and SWI-Prolog.
- W.P. Weijland (1990). "Semantics for Logic Programs without Occur Check" (PDF). Theoretical Computer Science 71: 155–174. doi:10.1016/0304-3975(90)90194-m.
- David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley.; here: p.143
- Informally, and taking to mean e.g. "x loves y", the formula reads "If everybody loves somebody, then a single person must exist that is loved by everyone."
- F. Pereira, D. Warren, D. Bowen, L. Byrd, L. Pereira (1983). C-Prolog's User's Manual Version 1.2 (Technical report). SRI International. Retrieved 21 June 2013.
- A. Colmerauer (1982). K.L. Clark and S.-A. Tarnlund, ed. Prolog and Infinite Trees. Academic Press.
- M.H. van Emden, J.W. Lloyd (1984). "A Logical Reconstruction of Prolog II". J. Logic Programming 2: 143–149.
- Joxan Jaffar, Peter J. Stuckey (1986). "Semantics of Infinite Tree Logic Programming". laeoretical Computer Science 46: 141–158. doi:10.1016/0304-3975(86)90027-7.
- B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Theoret. Comput. Sci. 25: 95–169. doi:10.1016/0304-3975(83)90059-2.