Быстрый алгоритм распознавания следствий для монадических логических программ

Установлен быстрый алгоритм, позволяющий за линейное время выяснять, является ли заданный литерал следствием монадической логической программы, т.е. программы, которая включает только одноместные символы предикатов и функций. Этот алгоритм можно использовать для распознавания допустимых управлений, если знание о целях и действиях системы представлено монадической программой.