Krysta, Piotr; Pacholski, Leszek The STO problem is NP-complete. (English) Zbl 0936.68020 J. Symb. Comput. 27, No. 2, 207-219 (1999). 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 PDF BibTeX XML Cite \textit{P. Krysta} and \textit{L. Pacholski}, J. Symb. Comput. 27, No. 2, 207--219 (1999; Zbl 0936.68020) Full Text: DOI