期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：42
页码：54-63
DOI：10.4204/EPTCS.42.5
出版社：Open Publishing Association
摘要：We prove that the Tiden and Arnborg algorithm for equational unification modulo one-sided distributivity is not polynomial time bounded as previously thought. A set of counterexamples is developed that demonstrates that the algorithm goes through exponentially many steps.
