On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity

Paliath Narendran
(University at Albany-SUNY)
Andrew Marshall
(University at Albany-SUNY)
Bibhu Mahapatra
(University at Albany-SUNY)

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.

In Maribel Fernandez: Proceedings 24th International Workshop on Unification (UNIF 2010), Edinburgh, United Kingdom, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 42, pp. 54–63.
Published: 21st December 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.42.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org