Усовершенствованный метод проверки выполнимости множества дизъюнктов в языке L.

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