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