On complexity of the anti-unification problem

In this paper we suggest a new algorithm of anti-unification of logic terms represented by acyclic directed graphs and estimate its complexity. The anti-unification problem consists of the following: for two given terms find the most specific term that has the given terms as instances. We suggest an anti-unification algorithm whose complexity linearly depends on the size of the most specific term it computes. It is thus established that the anti-unification problem is of almost the same complexity as the unification problem. It is also shown that there exist terms whose most specific term is of size $O(n^2)$, where $n$ is the size of the graphs representing these terms.