ИСТИНА

It is generally accepted that to unify a pair of substitutions 1 and 2 means to nd out a pair of substitutions 0 and 00 such that the compositions 10 and 200 are the same. Actually, unication is the problem of solving linear equations of the form 1X = 2Y in the semigroup of substitutions. But some other linear equations on substitutions may be also viewed as less common variants of unication problem. In this paper we introduce a two-sided unication as the process of bringing a given substitution 1 to another given substitution 2 from both sides by giving a solution to an equation X1Y = 2. Two- sided unication nds some applications in software refactoring as a means for extracting instances of library subroutines in arbitrary pieces of program code. In this paper we study the complexity of two-sided unication and show that this problem is NP-complete by reducing to it the bounded tiling problem.