アイテム詳細

要旨

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 an execution of the Martelli-Montanari unification algorithm gives for input $E$ a set $E^{\prime} \cup \{ x=t \}$, where $t \not= x$ and $x$ appears in $t$. Apt, van Emde Boas and Welling (1994) proved that STO is NP-hard leaving the problem of NP-completeness open.