Editing Occurs check (section)

==Sound unification==

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, provided the algorithm works correctly for all cases that are "not subject to occurs-check" (NSTO).<ref>7.3.4 Normal unification in Prolog of ISO/IEC 13211-1:1995.</ref> The built-in ''acyclic_term/1'' serves to check the finiteness of terms.

Implementations offering sound unification for all unifications are Qu-Prolog and [[Strawberry Prolog]] and (optionally, via a runtime flag): [[XSB]], [[SWI-Prolog]], [http://ctp.di.fct.unl.pt/~amd/cxprolog/ CxProlog], [http://tau-prolog.org/ Tau Prolog], [https://github.com/trealla-prolog/trealla Trealla Prolog] and [https://github.com/mthom/scryer-prolog/ Scryer Prolog]. A variety
<ref>{{cite journal|author1=Ritu Chadha |author2=David A. Plaisted | title=Correctness of unification without occur check in prolog| journal=The Journal of Logic Programming| year=1994| volume=18| issue=2| pages=99–122| doi=10.1016/0743-1066(94)90048-5| doi-access=free}}</ref><ref>{{cite conference|author1=Thomas Prokosch |author2=François Bry| title=Unification on the Run| conference=The 34th International Workshop on Unification| year=2020| pages=13:1–13:5| url=http://www3.risc.jku.at/publications/download/risc_6129/proceedings-UNIF2020.pdf}}</ref> of optimizations can render sound unification feasible for common cases.