The E-Unification problem appears in important application areas, e.g. automated deduction and cryptographic protocol analysis. As E-Unification is undecidable in general, there is an active search for decidable and, ideally, tractable instances of the problem.

In this dissertation we investigate a class of equational theories, which we call LM-Systems, that give rise to E-Unification problems solvable in polynomial time. This remarkable class of theories was first discovered by Dr. Christopher Lynch and Dr. Barbara Morawska in their paper ``Basic Syntactic Mutation". We adapt their definitions to convergent and forward-closed term-rewriting systems, and show that LM-Systems are highly restrictive. However, we also prove that the Cap Problem, a known undecidable problem from the field of cryptographic protocol analysis, remains undecidable when restricted to LM-Systems.

Motivated by the definition of LM-Systems, we next investigate the case of forward-closed and convergent string-rewriting systems. We show that the Subterm Collapse problem, which is undecidable for general convergent term-rewriting systems, becomes decidable when restricted to these systems. In particular, there is an algorithm to determine if such a string-rewriting system is an LM-System.

Finally, we show that the Finiteness of Forward-Closure problem, which is undecidable in general, is decidable for convergent and monadic string-rewriting systems.