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.
68N17 Logic programming
Full Text: DOI