Статья посвящена изложению алгоритма выделения максимальной общей с точностью до имён переменных подформулы двух элементарных конъюнкций атомарных предикатных формул. Предлагаемый алгоритм использует введённую ранее автором модификацию обратного метода Маслова, а также Муравьиные тактики и параллельные вычисления. Проблема выделения максимальной общей с точностью до имён переменных подформулы предикатных формул имеет достаточно широкое применение при построении эффективных алгоритмов решения задач искусственного интеллекта, допускающих формализацию средствами исчисления предикатов. Приведены асимптотические оценки числа шагов работы описанного алгоритма. С. 17-25.

The article is devoted to the describing of an algorithm which extract a maximal common up to the names of variables sub-formula of two elementary conjunctions of atomic predicate formulas. The offered algorithm uses the proposed earlier by the author modification of inverse method of S. Yu. Maslov as well as Ant tactics and concurrent processing. The problem of the extraction of a maximal common up to the names of variables sub-formula of predicate formulas has wide enough application while development of an effective algorithm solving an Artificial Intelligence problem permitting its description in the frameworks of predicate calculus language. Asymptotic estimates of the number of run steps for the described algorithm are formulated.