| The techniques and tools of unification theory have long been a core component of many areas of automated deduction and logic programming. In particular, equational unification with the purpose of dealing with unification modulo equational axioms is of critical importance to such areas as automated theorem proving and term rewriting. More recently unification has become important in formal verification, particularly in cryptographic protocol analysis.;We study the algorithmic and complexity issues of several equational theories with respect to the unification problem. Specifically, we study the one-sided distributive unification problem and the unification problem for modular exponentiation. We prove an exponential runtime bound on the algorithm developed by Tiden and Arnborg, for one-sided distributivity, demonstrating the previous polynomial runtime claim for this algorithm was incorrect. The result also implies the existence of exponential, with respect to the initial unification problem, most general unifiers. We next show that the decision form of the one-sided distributive unification problem is in P by developing a new algorithm with a polynomial bounded runtime. A construction, employing string compression, is used to achieve the polynomial bound. In addition, a new polynomial time algorithm for a variant of one-sided distributivity, called single homomorphism, is developed.;We next study a theory for modular exponentiation and develop a new unification algorithm for this theory. We then show that if this theory is extended in a natural way, by the addition of abelian group axioms for two of the operators, the unification problem becomes undecidable. These results help further define the boundary of what theories of exponentiation are usable in protocol analysis. |
