О сложности задачи антиунификации

В статье представлен новый алгоритм антиунификации логических выражений, представленных ациклическими ориентированными графами, и оценена его сложность. Задача антиунификации состоит в том, чтобы для двух заданных выражений отыскать наименее общее выражение (шаблон), примерами которого являются оба исходных выражения. Предложен алгоритм антиунификации, сложность которого линейно зависит от размера вычисляемого им наименее общего шаблона. Таким образом, устанавливается, что при измерении сложности алгоритмов относительно размеров исходных данных и вычисляемого результата задача антиунификации имеет почти такую же сложность, что и задача унификации. Показано также, что существуют такие выражения, наименее общий шаблон которых имеет размер $O(n^2)$, где $n$ – размер графов, представляющих исходные выражения.