Abstract
A finite set of term equations E is called subject to the occur-check (STO) if a sequence of actions of the Martelli-Montanari unification algorithm starts with E and ends with a failure due to occur-check. We prove here that the problem of deciding whether E is STO is NP-hard. © 1994 Academic Press Limited.
Cite
CITATION STYLE
APA
Apt, K. R., Boas, P. van E., & Welling, A. (1994). The STO-problem is NP-hard. Journal of Symbolic Computation, 18(5), 489–495. https://doi.org/10.1006/jsco.1994.1060
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free