# zbMATH — the first resource for mathematics

The STO problem is NP-complete. (English) Zbl 0936.68020
Summary: We prove that the problem STO of deciding whether or not a finite set $$E$$ of term equations is subject to occur-check is in NP. $$E$$ is subject to occur-check if the execution of the Martelli-Montanari unification algorithm gives for input $$E$$ a set $$E'\cup\{x= t\}$$, where $$t\neq x$$ and $$x$$ appears in $$t$$. K. R. Apt, P. van Emde Boas and A. Welling [J. Symb. Comput. 18, No. 5, 489-495 (1994; Zbl 0826.68030)] proved that STO is NP-hard leaving the problem of NP-completeness open. $$\copyright$$ Academic Press.
##### MSC:
 68N17 Logic programming
Full Text: