Аннотация:
Рассматривается задача проверки выводимости формул специального вида, к которым сводятся многие задачи искусственного интеллекта. Для еe решения применяется комбинация обратного метода С. Ю. Маслова проверки выводимости формул исчисления предикатов с муравьиными тактиками, позволяющими распараллеливать процесс построения вывода. Приводится алгоритм решения поставленной задачи. Доказываются оценки числа шагов их работы. Описывается пример решения модельной задачи с помощью предложенного алгоритма. Библиогр. 7 назв. Ил. 2.